DEFINITION pr2_change()
TYPE =
∀b:B
.not (eq B b Abbr)
→∀c:C.∀v1:T.∀t1:T.∀t2:T.(pr2 (CHead c (Bind b) v1) t1 t2)→∀v2:T.(pr2 (CHead c (Bind b) v2) t1 t2)
BODY =
assume b: B
suppose H: not (eq B b Abbr)
assume c: C
assume v1: T
assume t1: T
assume t2: T
suppose H0: pr2 (CHead c (Bind b) v1) t1 t2
assume v2: T
assume y: C
suppose H1: pr2 y t1 t2
we proceed by induction on H1 to prove (eq C y (CHead c (Bind b) v1))→(pr2 (CHead c (Bind b) v2) t1 t2)
case pr2_free : c0:C t3:T t4:T H2:pr0 t3 t4 ⇒
the thesis becomes (eq C c0 (CHead c (Bind b) v1))→(pr2 (CHead c (Bind b) v2) t3 t4)
suppose : eq C c0 (CHead c (Bind b) v1)
by (pr2_free . . . H2)
we proved pr2 (CHead c (Bind b) v2) t3 t4
(eq C c0 (CHead c (Bind b) v1))→(pr2 (CHead c (Bind b) v2) t3 t4)
case pr2_delta : c0:C d:C u:T i:nat H2:getl i c0 (CHead d (Bind Abbr) u) t3:T t4:T H3:pr0 t3 t4 t:T H4:subst0 i u t4 t ⇒
the thesis becomes ∀H5:(eq C c0 (CHead c (Bind b) v1)).(pr2 (CHead c (Bind b) v2) t3 t)
suppose H5: eq C c0 (CHead c (Bind b) v1)
(H6)
we proceed by induction on H5 to prove getl i (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
getl i (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)
end of H6
suppose H7: getl O (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)
suppose H8: subst0 O u t4 t
(H9)
by (getl_gen_O . . H7)
we proved clear (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead d (Bind Abbr) u) (CHead c (Bind b) v1)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead c (Bind b) v1 OF CSort ⇒d | CHead c1 ⇒c1
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead d (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead c (Bind b) v1)
end of H9
(h1)
(H10)
by (getl_gen_O . . H7)
we proved clear (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead d (Bind Abbr) u) (CHead c (Bind b) v1)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c (Bind b) v1 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
CHead d (Bind Abbr) u
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
CHead c (Bind b) v1
end of H10
(h1)
(H11)
by (getl_gen_O . . H7)
we proved clear (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead d (Bind Abbr) u) (CHead c (Bind b) v1)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead c (Bind b) v1 OF CSort ⇒u | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead d (Bind Abbr) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead c (Bind b) v1)
end of H11
suppose H12: eq B Abbr b
suppose : eq C d c
(H15)
by (eq_ind_r . . . H . H12)
not (eq B Abbr Abbr)
end of H15
we proceed by induction on H12 to prove pr2 (CHead c (Bind b) v2) t3 t
case refl_equal : ⇒
the thesis becomes pr2 (CHead c (Bind Abbr) v2) t3 t
(H16)
by (refl_equal . .)
we proved eq B Abbr Abbr
by (H15 previous)
we proved False
by cases on the previous result we prove pr2 (CHead c (Bind Abbr) v2) t3 t
pr2 (CHead c (Bind Abbr) v2) t3 t
end of H16
consider H16
pr2 (CHead c (Bind Abbr) v2) t3 t
we proved pr2 (CHead c (Bind b) v2) t3 t
(eq B Abbr b)→(eq C d c)→(pr2 (CHead c (Bind b) v2) t3 t)
end of h1
(h2)
consider H10
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c (Bind b) v1 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
eq B Abbr b
end of h2
by (h1 h2)
(eq C d c)→(pr2 (CHead c (Bind b) v2) t3 t)
end of h1
(h2)
consider H9
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead c (Bind b) v1 OF CSort ⇒d | CHead c1 ⇒c1
eq C d c
end of h2
by (h1 h2)
we proved pr2 (CHead c (Bind b) v2) t3 t
getl O (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)
→(subst0 O u t4 t)→(pr2 (CHead c (Bind b) v2) t3 t)
assume i0: nat
suppose :
getl i0 (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)
→(subst0 i0 u t4 t)→(pr2 (CHead c (Bind b) v2) t3 t)
suppose H7: getl (S i0) (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)
suppose H8: subst0 (S i0) u t4 t
by (getl_gen_S . . . . . H7)
we proved getl (r (Bind b) i0) c (CHead d (Bind Abbr) u)
by (getl_head . . . . previous .)
we proved getl (S i0) (CHead c (Bind b) v2) (CHead d (Bind Abbr) u)
by (pr2_delta . . . . previous . . H3 . H8)
we proved pr2 (CHead c (Bind b) v2) t3 t
∀H7:getl (S i0) (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)
.∀H8:(subst0 (S i0) u t4 t).(pr2 (CHead c (Bind b) v2) t3 t)
by (previous . H6 H4)
we proved pr2 (CHead c (Bind b) v2) t3 t
∀H5:(eq C c0 (CHead c (Bind b) v1)).(pr2 (CHead c (Bind b) v2) t3 t)
we proved (eq C y (CHead c (Bind b) v1))→(pr2 (CHead c (Bind b) v2) t1 t2)
we proved
∀y:C
.pr2 y t1 t2
→(eq C y (CHead c (Bind b) v1))→(pr2 (CHead c (Bind b) v2) t1 t2)
by (insert_eq . . . . previous H0)
we proved pr2 (CHead c (Bind b) v2) t1 t2
we proved
∀b:B
.not (eq B b Abbr)
→∀c:C.∀v1:T.∀t1:T.∀t2:T.(pr2 (CHead c (Bind b) v1) t1 t2)→∀v2:T.(pr2 (CHead c (Bind b) v2) t1 t2)