DEFINITION pr3_pr2_pr2_t()
TYPE =
∀c:C.∀u1:T.∀u2:T.(pr2 c u1 u2)→∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u2) t1 t2)→(pr3 (CHead c k u1) t1 t2)
BODY =
assume c: C
assume u1: T
assume u2: T
suppose H: pr2 c u1 u2
we proceed by induction on H to prove ∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u2) t1 t2)→(pr3 (CHead c k u1) t1 t2)
case pr2_free : c0:C t1:T t2:T H0:pr0 t1 t2 ⇒
the thesis becomes ∀t0:T.∀t3:T.∀k:K.∀H1:(pr2 (CHead c0 k t2) t0 t3).(pr3 (CHead c0 k t1) t0 t3)
assume t0: T
assume t3: T
assume k: K
suppose H1: pr2 (CHead c0 k t2) t0 t3
by (pr3_pr0_pr2_t . . H0 . . . . H1)
we proved pr3 (CHead c0 k t1) t0 t3
∀t0:T.∀t3:T.∀k:K.∀H1:(pr2 (CHead c0 k t2) t0 t3).(pr3 (CHead c0 k t1) t0 t3)
case pr2_delta : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u) t1:T t2:T H1:pr0 t1 t2 t:T H2:subst0 i u t2 t ⇒
the thesis becomes ∀t0:T.∀t3:T.∀k:K.∀H3:(pr2 (CHead c0 k t) t0 t3).(pr3 (CHead c0 k t1) t0 t3)
assume t0: T
assume t3: T
assume k: K
suppose H3: pr2 (CHead c0 k t) t0 t3
assume y: C
suppose H4: pr2 y t0 t3
we proceed by induction on H4 to prove (eq C y (CHead c0 k t))→(pr3 (CHead c0 k t1) t0 t3)
case pr2_free : c1:C t4:T t5:T H5:pr0 t4 t5 ⇒
the thesis becomes (eq C c1 (CHead c0 k t))→(pr3 (CHead c0 k t1) t4 t5)
suppose : eq C c1 (CHead c0 k t)
by (pr2_free . . . H5)
we proved pr2 (CHead c0 k t1) t4 t5
by (pr3_pr2 . . . previous)
we proved pr3 (CHead c0 k t1) t4 t5
(eq C c1 (CHead c0 k t))→(pr3 (CHead c0 k t1) t4 t5)
case pr2_delta : c1:C d0:C u0:T i0:nat H5:getl i0 c1 (CHead d0 (Bind Abbr) u0) t4:T t5:T H6:pr0 t4 t5 t6:T H7:subst0 i0 u0 t5 t6 ⇒
the thesis becomes ∀H8:(eq C c1 (CHead c0 k t)).(pr3 (CHead c0 k t1) t4 t6)
suppose H8: eq C c1 (CHead c0 k t)
(H9)
we proceed by induction on H8 to prove getl i0 (CHead c0 k t) (CHead d0 (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
getl i0 (CHead c0 k t) (CHead d0 (Bind Abbr) u0)
end of H9
suppose H10: getl O (CHead c0 k t) (CHead d0 (Bind Abbr) u0)
suppose H11: subst0 O u0 t5 t6
by (getl_gen_O . . H10)
we proved clear (CHead c0 k t) (CHead d0 (Bind Abbr) u0)
assume b: B
suppose H12: clear (CHead c0 (Bind b) t) (CHead d0 (Bind Abbr) u0)
(H13)
by (clear_gen_bind . . . . H12)
we proved eq C (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒d0 | CHead c2 ⇒c2
<λ:C.C> CASE CHead c0 (Bind b) t OF CSort ⇒d0 | CHead c2 ⇒c2
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d0 | CHead c2 ⇒c2 (CHead d0 (Bind Abbr) u0)
λe:C.<λ:C.C> CASE e OF CSort ⇒d0 | CHead c2 ⇒c2 (CHead c0 (Bind b) t)
end of H13
(h1)
(H14)
by (clear_gen_bind . . . . H12)
we proved eq C (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d0 (Bind Abbr) u0 OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c0 (Bind b) t OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
CHead d0 (Bind Abbr) u0
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
CHead c0 (Bind b) t
end of H14
(h1)
(H15)
by (clear_gen_bind . . . . H12)
we proved eq C (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒u0 | CHead t7⇒t7
<λ:C.T> CASE CHead c0 (Bind b) t OF CSort ⇒u0 | CHead t7⇒t7
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t7⇒t7 (CHead d0 (Bind Abbr) u0)
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t7⇒t7 (CHead c0 (Bind b) t)
end of H15
suppose H16: eq B Abbr b
suppose : eq C d0 c0
(H18)
consider H15
we proved
eq
T
<λ:C.T> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒u0 | CHead t7⇒t7
<λ:C.T> CASE CHead c0 (Bind b) t OF CSort ⇒u0 | CHead t7⇒t7
that is equivalent to eq T u0 t
we proceed by induction on the previous result to prove subst0 O t t5 t6
case refl_equal : ⇒
the thesis becomes the hypothesis H11
subst0 O t t5 t6
end of H18
we proceed by induction on H16 to prove pr3 (CHead c0 (Bind b) t1) t4 t6
case refl_equal : ⇒
the thesis becomes pr3 (CHead c0 (Bind Abbr) t1) t4 t6
by (subst0_subst0 . . . . H18 . . . H2)
we proved ex2 T λt:T.subst0 O t2 t5 t λt:T.subst0 (S (plus i O)) u t t6
we proceed by induction on the previous result to prove pr3 (CHead c0 (Bind Abbr) t1) t4 t6
case ex_intro2 : x:T H19:subst0 O t2 t5 x H20:subst0 (S (plus i O)) u x t6 ⇒
the thesis becomes pr3 (CHead c0 (Bind Abbr) t1) t4 t6
(H21)
by (plus_n_O .)
we proved eq nat i (plus i O)
by (sym_eq . . . previous)
we proved eq nat (plus i O) i
by (f_equal . . . . . previous)
eq nat (S (plus i O)) (S i)
end of H21
(H22)
we proceed by induction on H21 to prove subst0 (S i) u x t6
case refl_equal : ⇒
the thesis becomes the hypothesis H20
subst0 (S i) u x t6
end of H22
by (pr0_subst0_back . . . . H19 . H1)
we proved ex2 T λt:T.subst0 O t1 t5 t λt:T.pr0 t x
we proceed by induction on the previous result to prove pr3 (CHead c0 (Bind Abbr) t1) t4 t6
case ex_intro2 : x0:T H23:subst0 O t1 t5 x0 H24:pr0 x0 x ⇒
the thesis becomes pr3 (CHead c0 (Bind Abbr) t1) t4 t6
(h1)
by (getl_refl . . .)
we proved getl O (CHead c0 (Bind Abbr) t1) (CHead c0 (Bind Abbr) t1)
by (pr2_delta . . . . previous . . H6 . H23)
pr2 (CHead c0 (Bind Abbr) t1) t4 x0
end of h1
(h2)
by (clear_bind . . .)
we proved clear (CHead c0 (Bind Abbr) t1) (CHead c0 (Bind Abbr) t1)
by (getl_clear_bind . . . . previous . . H0)
we proved getl (S i) (CHead c0 (Bind Abbr) t1) (CHead d (Bind Abbr) u)
by (pr2_delta . . . . previous . . H24 . H22)
we proved pr2 (CHead c0 (Bind Abbr) t1) x0 t6
by (pr3_pr2 . . . previous)
pr3 (CHead c0 (Bind Abbr) t1) x0 t6
end of h2
by (pr3_sing . . . h1 . h2)
pr3 (CHead c0 (Bind Abbr) t1) t4 t6
pr3 (CHead c0 (Bind Abbr) t1) t4 t6
pr3 (CHead c0 (Bind Abbr) t1) t4 t6
we proved pr3 (CHead c0 (Bind b) t1) t4 t6
(eq B Abbr b)→(eq C d0 c0)→(pr3 (CHead c0 (Bind b) t1) t4 t6)
end of h1
(h2)
consider H14
we proved
eq
B
<λ:C.B>
CASE CHead d0 (Bind Abbr) u0 OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c0 (Bind b) t OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
eq B Abbr b
end of h2
by (h1 h2)
(eq C d0 c0)→(pr3 (CHead c0 (Bind b) t1) t4 t6)
end of h1
(h2)
consider H13
we proved
eq
C
<λ:C.C> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒d0 | CHead c2 ⇒c2
<λ:C.C> CASE CHead c0 (Bind b) t OF CSort ⇒d0 | CHead c2 ⇒c2
eq C d0 c0
end of h2
by (h1 h2)
we proved pr3 (CHead c0 (Bind b) t1) t4 t6
∀H12:clear (CHead c0 (Bind b) t) (CHead d0 (Bind Abbr) u0)
.pr3 (CHead c0 (Bind b) t1) t4 t6
assume f: F
suppose H12: clear (CHead c0 (Flat f) t) (CHead d0 (Bind Abbr) u0)
(h1)
by (drop_refl .)
drop O O c0 c0
end of h1
(h2)
by (clear_gen_flat . . . . H12)
clear c0 (CHead d0 (Bind Abbr) u0)
end of h2
by (getl_intro . . . . h1 h2)
we proved getl O c0 (CHead d0 (Bind Abbr) u0)
by (pr2_delta . . . . previous . . H6 . H11)
we proved pr2 c0 t4 t6
by (pr2_cflat . . . previous . .)
we proved pr2 (CHead c0 (Flat f) t1) t4 t6
by (pr3_pr2 . . . previous)
we proved pr3 (CHead c0 (Flat f) t1) t4 t6
∀H12:clear (CHead c0 (Flat f) t) (CHead d0 (Bind Abbr) u0)
.pr3 (CHead c0 (Flat f) t1) t4 t6
by (previous . previous)
we proved pr3 (CHead c0 k t1) t4 t6
getl O (CHead c0 k t) (CHead d0 (Bind Abbr) u0)
→(subst0 O u0 t5 t6)→(pr3 (CHead c0 k t1) t4 t6)
assume i1: nat
suppose :
getl i1 (CHead c0 k t) (CHead d0 (Bind Abbr) u0)
→(subst0 i1 u0 t5 t6)→(pr3 (CHead c0 k t1) t4 t6)
suppose H10: getl (S i1) (CHead c0 k t) (CHead d0 (Bind Abbr) u0)
suppose H11: subst0 (S i1) u0 t5 t6
assume b: B
suppose H12: getl (S i1) (CHead c0 (Bind b) t) (CHead d0 (Bind Abbr) u0)
by (getl_gen_S . . . . . H12)
we proved getl (r (Bind b) i1) c0 (CHead d0 (Bind Abbr) u0)
by (getl_head . . . . previous .)
we proved getl (S i1) (CHead c0 (Bind b) t1) (CHead d0 (Bind Abbr) u0)
by (pr2_delta . . . . previous . . H6 . H11)
we proved pr2 (CHead c0 (Bind b) t1) t4 t6
by (pr3_pr2 . . . previous)
we proved pr3 (CHead c0 (Bind b) t1) t4 t6
∀H12:getl (S i1) (CHead c0 (Bind b) t) (CHead d0 (Bind Abbr) u0)
.pr3 (CHead c0 (Bind b) t1) t4 t6
assume f: F
suppose H12: getl (S i1) (CHead c0 (Flat f) t) (CHead d0 (Bind Abbr) u0)
(h1)
by (getl_gen_S . . . . . H12)
getl (r (Flat f) i1) c0 (CHead d0 (Bind Abbr) u0)
end of h1
(h2)
consider H11
we proved subst0 (S i1) u0 t5 t6
subst0 (r (Flat f) i1) u0 t5 t6
end of h2
by (pr2_delta . . . . h1 . . H6 . h2)
we proved pr2 c0 t4 t6
by (pr2_cflat . . . previous . .)
we proved pr2 (CHead c0 (Flat f) t1) t4 t6
by (pr3_pr2 . . . previous)
we proved pr3 (CHead c0 (Flat f) t1) t4 t6
∀H12:getl (S i1) (CHead c0 (Flat f) t) (CHead d0 (Bind Abbr) u0)
.pr3 (CHead c0 (Flat f) t1) t4 t6
by (previous . H10)
we proved pr3 (CHead c0 k t1) t4 t6
∀H10:getl (S i1) (CHead c0 k t) (CHead d0 (Bind Abbr) u0)
.∀H11:(subst0 (S i1) u0 t5 t6).(pr3 (CHead c0 k t1) t4 t6)
by (previous . H9 H7)
we proved pr3 (CHead c0 k t1) t4 t6
∀H8:(eq C c1 (CHead c0 k t)).(pr3 (CHead c0 k t1) t4 t6)
we proved (eq C y (CHead c0 k t))→(pr3 (CHead c0 k t1) t0 t3)
we proved ∀y:C.(pr2 y t0 t3)→(eq C y (CHead c0 k t))→(pr3 (CHead c0 k t1) t0 t3)
by (insert_eq . . . . previous H3)
we proved pr3 (CHead c0 k t1) t0 t3
∀t0:T.∀t3:T.∀k:K.∀H3:(pr2 (CHead c0 k t) t0 t3).(pr3 (CHead c0 k t1) t0 t3)
we proved ∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u2) t1 t2)→(pr3 (CHead c k u1) t1 t2)
we proved ∀c:C.∀u1:T.∀u2:T.(pr2 c u1 u2)→∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u2) t1 t2)→(pr3 (CHead c k u1) t1 t2)