DEFINITION ty3_sred_wcpr0_pr0()
TYPE =
∀g:G.∀c1:C.∀t1:T.∀t:T.(ty3 g c1 t1 t)→∀c2:C.(wcpr0 c1 c2)→∀t2:T.(pr0 t1 t2)→(ty3 g c2 t2 t)
BODY =
assume g: G
assume c1: C
assume t1: T
assume t: T
suppose H: ty3 g c1 t1 t
we proceed by induction on H to prove ∀c2:C.(wcpr0 c1 c2)→∀t3:T.(pr0 t1 t3)→(ty3 g c2 t3 t)
case ty3_conv : c:C t2:T t0:T :ty3 g c t2 t0 u:T t3:T :ty3 g c u t3 H4:pc3 c t3 t2 ⇒
the thesis becomes ∀c2:C.∀H5:(wcpr0 c c2).∀t4:T.∀H6:(pr0 u t4).(ty3 g c2 t4 t2)
(H1) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t3:T.(pr0 t2 t3)→(ty3 g c2 t3 t0)
(H3) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t4:T.(pr0 u t4)→(ty3 g c2 t4 t3)
assume c2: C
suppose H5: wcpr0 c c2
assume t4: T
suppose H6: pr0 u t4
(h1)
by (pr0_refl .)
we proved pr0 t2 t2
by (H1 . H5 . previous)
ty3 g c2 t2 t0
end of h1
(h2) by (H3 . H5 . H6) we proved ty3 g c2 t4 t3
(h3) by (pc3_wcpr0 . . H5 . . H4) we proved pc3 c2 t3 t2
by (ty3_conv . . . . h1 . . h2 h3)
we proved ty3 g c2 t4 t2
∀c2:C.∀H5:(wcpr0 c c2).∀t4:T.∀H6:(pr0 u t4).(ty3 g c2 t4 t2)
case ty3_sort : c:C m:nat ⇒
the thesis becomes ∀c2:C.(wcpr0 c c2)→∀t2:T.∀H1:(pr0 (TSort m) t2).(ty3 g c2 t2 (TSort (next g m)))
assume c2: C
suppose : wcpr0 c c2
assume t2: T
suppose H1: pr0 (TSort m) t2
(h1)
by (ty3_sort . . .)
ty3 g c2 (TSort m) (TSort (next g m))
end of h1
(h2)
by (pr0_gen_sort . . H1)
eq T t2 (TSort m)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ty3 g c2 t2 (TSort (next g m))
∀c2:C.(wcpr0 c c2)→∀t2:T.∀H1:(pr0 (TSort m) t2).(ty3 g c2 t2 (TSort (next g m)))
case ty3_abbr : n:nat c:C d:C u:T H0:getl n c (CHead d (Bind Abbr) u) t0:T :ty3 g d u t0 ⇒
the thesis becomes ∀c2:C.∀H3:(wcpr0 c c2).∀t2:T.∀H4:(pr0 (TLRef n) t2).(ty3 g c2 t2 (lift (S n) O t0))
(H2) by induction hypothesis we know ∀c2:C.(wcpr0 d c2)→∀t2:T.(pr0 u t2)→(ty3 g c2 t2 t0)
assume c2: C
suppose H3: wcpr0 c c2
assume t2: T
suppose H4: pr0 (TLRef n) t2
(h1)
by (wcpr0_getl . . H3 . . . . H0)
we proved ex3_2 C T λe2:C.λu2:T.getl n c2 (CHead e2 (Bind Abbr) u2) λe2:C.λ:T.wcpr0 d e2 λ:C.λu2:T.pr0 u u2
we proceed by induction on the previous result to prove ty3 g c2 (TLRef n) (lift (S n) O t0)
case ex3_2_intro : x0:C x1:T H5:getl n c2 (CHead x0 (Bind Abbr) x1) H6:wcpr0 d x0 H7:pr0 u x1 ⇒
the thesis becomes ty3 g c2 (TLRef n) (lift (S n) O t0)
by (H2 . H6 . H7)
we proved ty3 g x0 x1 t0
by (ty3_abbr . . . . . H5 . previous)
ty3 g c2 (TLRef n) (lift (S n) O t0)
ty3 g c2 (TLRef n) (lift (S n) O t0)
end of h1
(h2)
by (pr0_gen_lref . . H4)
eq T t2 (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ty3 g c2 t2 (lift (S n) O t0)
∀c2:C.∀H3:(wcpr0 c c2).∀t2:T.∀H4:(pr0 (TLRef n) t2).(ty3 g c2 t2 (lift (S n) O t0))
case ty3_abst : n:nat c:C d:C u:T H0:getl n c (CHead d (Bind Abst) u) t0:T :ty3 g d u t0 ⇒
the thesis becomes ∀c2:C.∀H3:(wcpr0 c c2).∀t2:T.∀H4:(pr0 (TLRef n) t2).(ty3 g c2 t2 (lift (S n) O u))
(H2) by induction hypothesis we know ∀c2:C.(wcpr0 d c2)→∀t2:T.(pr0 u t2)→(ty3 g c2 t2 t0)
assume c2: C
suppose H3: wcpr0 c c2
assume t2: T
suppose H4: pr0 (TLRef n) t2
(h1)
by (wcpr0_getl . . H3 . . . . H0)
we proved ex3_2 C T λe2:C.λu2:T.getl n c2 (CHead e2 (Bind Abst) u2) λe2:C.λ:T.wcpr0 d e2 λ:C.λu2:T.pr0 u u2
we proceed by induction on the previous result to prove ty3 g c2 (TLRef n) (lift (S n) O u)
case ex3_2_intro : x0:C x1:T H5:getl n c2 (CHead x0 (Bind Abst) x1) H6:wcpr0 d x0 H7:pr0 u x1 ⇒
the thesis becomes ty3 g c2 (TLRef n) (lift (S n) O u)
(h1)
(h1)
by (pr0_refl .)
we proved pr0 u u
by (H2 . H6 . previous)
ty3 g x0 u t0
end of h1
(h2)
by (getl_drop . . . . . H5)
drop (S n) O c2 x0
end of h2
by (ty3_lift . . . . h1 . . . h2)
ty3 g c2 (lift (S n) O u) (lift (S n) O t0)
end of h1
(h2)
by (H2 . H6 . H7)
we proved ty3 g x0 x1 t0
by (ty3_abst . . . . . H5 . previous)
ty3 g c2 (TLRef n) (lift (S n) O x1)
end of h2
(h3)
(h1)
by (getl_drop . . . . . H5)
drop (S n) O c2 x0
end of h1
(h2)
by (pr2_free . . . H7)
we proved pr2 x0 u x1
by (pc3_pr2_x . . . previous)
pc3 x0 x1 u
end of h2
by (pc3_lift . . . . h1 . . h2)
pc3 c2 (lift (S n) O x1) (lift (S n) O u)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c2 (TLRef n) (lift (S n) O u)
ty3 g c2 (TLRef n) (lift (S n) O u)
end of h1
(h2)
by (pr0_gen_lref . . H4)
eq T t2 (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ty3 g c2 t2 (lift (S n) O u)
∀c2:C.∀H3:(wcpr0 c c2).∀t2:T.∀H4:(pr0 (TLRef n) t2).(ty3 g c2 t2 (lift (S n) O u))
case ty3_bind : c:C u:T t0:T :ty3 g c u t0 b:B t2:T t3:T H2:ty3 g (CHead c (Bind b) u) t2 t3 ⇒
the thesis becomes ∀c2:C.∀H4:(wcpr0 c c2).∀t4:T.∀H5:(pr0 (THead (Bind b) u t2) t4).(ty3 g c2 t4 (THead (Bind b) u t3))
(H1) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t2:T.(pr0 u t2)→(ty3 g c2 t2 t0)
(H3) by induction hypothesis we know ∀c2:C.(wcpr0 (CHead c (Bind b) u) c2)→∀t4:T.(pr0 t2 t4)→(ty3 g c2 t4 t3)
assume c2: C
suppose H4: wcpr0 c c2
assume t4: T
suppose H5: pr0 (THead (Bind b) u t2) t4
(H6)
by cases on H5 we prove
eq T (THead (Bind b) u t2) (THead (Bind b) u t2)
→(eq T t4 t4)→(ty3 g c2 t4 (THead (Bind b) u t3))
case pr0_refl t5:T ⇒
the thesis becomes ∀H6:(eq T t5 (THead (Bind b) u t2)).∀H7:(eq T t5 t4).(ty3 g c2 t4 (THead (Bind b) u t3))
suppose H6: eq T t5 (THead (Bind b) u t2)
suppose H7: eq T t5 t4
by (sym_eq . . . H6)
we proved eq T (THead (Bind b) u t2) t5
suppose H8: eq T (THead (Bind b) u t2) t4
we proceed by induction on H8 to prove ty3 g c2 t4 (THead (Bind b) u t3)
case refl_equal : ⇒
the thesis becomes ty3 g c2 (THead (Bind b) u t2) (THead (Bind b) u t3)
(h1)
by (pr0_refl .)
we proved pr0 u u
by (H1 . H4 . previous)
ty3 g c2 u t0
end of h1
(h2)
(h1)
by (pr0_refl .)
we proved pr0 u u
by (wcpr0_comp . . H4 . . previous .)
wcpr0 (CHead c (Bind b) u) (CHead c2 (Bind b) u)
end of h1
(h2) by (pr0_refl .) we proved pr0 t2 t2
by (H3 . h1 . h2)
ty3 g (CHead c2 (Bind b) u) t2 t3
end of h2
by (ty3_bind . . . . h1 . . . h2)
ty3 g c2 (THead (Bind b) u t2) (THead (Bind b) u t3)
we proved ty3 g c2 t4 (THead (Bind b) u t3)
(eq T (THead (Bind b) u t2) t4)→(ty3 g c2 t4 (THead (Bind b) u t3))
by (previous previous H7)
we proved ty3 g c2 t4 (THead (Bind b) u t3)
∀H6:(eq T t5 (THead (Bind b) u t2)).∀H7:(eq T t5 t4).(ty3 g c2 t4 (THead (Bind b) u t3))
case pr0_comp u1:T u2:T H6:pr0 u1 u2 t5:T t6:T H7:pr0 t5 t6 k:K ⇒
the thesis becomes
∀H8:eq T (THead k u1 t5) (THead (Bind b) u t2)
.∀H9:(eq T (THead k u2 t6) t4).(ty3 g c2 t4 (THead (Bind b) u t3))
suppose H8: eq T (THead k u1 t5) (THead (Bind b) u t2)
suppose H9: eq T (THead k u2 t6) t4
(H10)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead k u1 t5 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
<λ:T.T> CASE THead (Bind b) u t2 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7 (THead k u1 t5)
λe:T.<λ:T.T> CASE e OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
THead (Bind b) u t2
end of H10
(h1)
(H11)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead k u1 t5 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
<λ:T.T> CASE THead (Bind b) u t2 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7 (THead k u1 t5)
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
THead (Bind b) u t2
end of H11
(h1)
(H12)
by (f_equal . . . . . H8)
we proved
eq
K
<λ:T.K> CASE THead k u1 t5 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K> CASE THead (Bind b) u t2 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0 (THead k u1 t5)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
THead (Bind b) u t2
end of H12
consider H12
we proved
eq
K
<λ:T.K> CASE THead k u1 t5 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K> CASE THead (Bind b) u t2 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
that is equivalent to eq K k (Bind b)
by (sym_eq . . . previous)
we proved eq K (Bind b) k
we proceed by induction on the previous result to prove
eq T u1 u
→(eq T t5 t2
→(eq T (THead k u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))))
case refl_equal : ⇒
the thesis becomes
eq T u1 u
→(eq T t5 t2
→(eq T (THead (Bind b) u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))))
suppose H13: eq T u1 u
by (sym_eq . . . H13)
we proved eq T u u1
we proceed by induction on the previous result to prove
eq T t5 t2
→(eq T (THead (Bind b) u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
case refl_equal : ⇒
the thesis becomes
eq T t5 t2
→(eq T (THead (Bind b) u2 t6) t4
→(pr0 u u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
suppose H14: eq T t5 t2
by (sym_eq . . . H14)
we proved eq T t2 t5
we proceed by induction on the previous result to prove
eq T (THead (Bind b) u2 t6) t4
→(pr0 u u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
case refl_equal : ⇒
the thesis becomes
eq T (THead (Bind b) u2 t6) t4
→(pr0 u u2)→(pr0 t2 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
suppose H15: eq T (THead (Bind b) u2 t6) t4
we proceed by induction on H15 to prove (pr0 u u2)→(pr0 t2 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
case refl_equal : ⇒
the thesis becomes (pr0 u u2)→(pr0 t2 t6)→(ty3 g c2 (THead (Bind b) u2 t6) (THead (Bind b) u t3))
suppose H16: pr0 u u2
suppose H17: pr0 t2 t6
(h1)
by (pr0_refl .)
we proved pr0 u u
by (wcpr0_comp . . H4 . . previous .)
wcpr0 (CHead c (Bind b) u) (CHead c2 (Bind b) u)
end of h1
(h2) by (pr0_refl .) we proved pr0 t2 t2
by (H3 . h1 . h2)
we proved ty3 g (CHead c2 (Bind b) u) t2 t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c2 (Bind b) u) t3 t
we proceed by induction on the previous result to prove ty3 g c2 (THead (Bind b) u2 t6) (THead (Bind b) u t3)
case ex_intro : x:T H18:ty3 g (CHead c2 (Bind b) u) t3 x ⇒
the thesis becomes ty3 g c2 (THead (Bind b) u2 t6) (THead (Bind b) u t3)
by (wcpr0_comp . . H4 . . H16 .)
we proved wcpr0 (CHead c (Bind b) u) (CHead c2 (Bind b) u2)
by (H3 . previous . H17)
we proved ty3 g (CHead c2 (Bind b) u2) t6 t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c2 (Bind b) u2) t3 t
we proceed by induction on the previous result to prove ty3 g c2 (THead (Bind b) u2 t6) (THead (Bind b) u t3)
case ex_intro : x0:T :ty3 g (CHead c2 (Bind b) u2) t3 x0 ⇒
the thesis becomes ty3 g c2 (THead (Bind b) u2 t6) (THead (Bind b) u t3)
(h1)
by (pr0_refl .)
we proved pr0 u u
by (H1 . H4 . previous)
we proved ty3 g c2 u t0
by (ty3_bind . . . . previous . . . H18)
ty3 g c2 (THead (Bind b) u t3) (THead (Bind b) u x)
end of h1
(h2)
(h1) by (H1 . H4 . H16) we proved ty3 g c2 u2 t0
(h2)
by (wcpr0_comp . . H4 . . H16 .)
we proved wcpr0 (CHead c (Bind b) u) (CHead c2 (Bind b) u2)
by (H3 . previous . H17)
ty3 g (CHead c2 (Bind b) u2) t6 t3
end of h2
by (ty3_bind . . . . h1 . . . h2)
ty3 g c2 (THead (Bind b) u2 t6) (THead (Bind b) u2 t3)
end of h2
(h3)
by (pr2_free . . . H16)
we proved pr2 c2 u u2
by (pr2_head_1 . . . previous . .)
we proved pr2 c2 (THead (Bind b) u t3) (THead (Bind b) u2 t3)
by (pc3_pr2_x . . . previous)
pc3 c2 (THead (Bind b) u2 t3) (THead (Bind b) u t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c2 (THead (Bind b) u2 t6) (THead (Bind b) u t3)
ty3 g c2 (THead (Bind b) u2 t6) (THead (Bind b) u t3)
we proved ty3 g c2 (THead (Bind b) u2 t6) (THead (Bind b) u t3)
(pr0 u u2)→(pr0 t2 t6)→(ty3 g c2 (THead (Bind b) u2 t6) (THead (Bind b) u t3))
we proved (pr0 u u2)→(pr0 t2 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
eq T (THead (Bind b) u2 t6) t4
→(pr0 u u2)→(pr0 t2 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
we proved
eq T (THead (Bind b) u2 t6) t4
→(pr0 u u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
eq T t5 t2
→(eq T (THead (Bind b) u2 t6) t4
→(pr0 u u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
we proved
eq T t5 t2
→(eq T (THead (Bind b) u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
eq T u1 u
→(eq T t5 t2
→(eq T (THead (Bind b) u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))))
eq T u1 u
→(eq T t5 t2
→(eq T (THead k u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))))
end of h1
(h2)
consider H11
we proved
eq
T
<λ:T.T> CASE THead k u1 t5 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
<λ:T.T> CASE THead (Bind b) u t2 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
eq T u1 u
end of h2
by (h1 h2)
eq T t5 t2
→(eq T (THead k u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
end of h1
(h2)
consider H10
we proved
eq
T
<λ:T.T> CASE THead k u1 t5 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
<λ:T.T> CASE THead (Bind b) u t2 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
eq T t5 t2
end of h2
by (h1 h2)
we proved
eq T (THead k u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
by (previous H9 H6 H7)
we proved ty3 g c2 t4 (THead (Bind b) u t3)
∀H8:eq T (THead k u1 t5) (THead (Bind b) u t2)
.∀H9:(eq T (THead k u2 t6) t4).(ty3 g c2 t4 (THead (Bind b) u t3))
case pr0_beta u0:T v1:T v2:T H6:pr0 v1 v2 t5:T t6:T H7:pr0 t5 t6 ⇒
the thesis becomes
∀H8:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t5)
THead (Bind b) u t2
.∀H9:(eq T (THead (Bind Abbr) v2 t6) t4).(ty3 g c2 t4 (THead (Bind b) u t3))
suppose H8:
eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t5)
THead (Bind b) u t2
suppose H9: eq T (THead (Bind Abbr) v2 t6) t4
(H10)
we proceed by induction on H8 to prove
<λ:T.Prop>
CASE THead (Bind b) u t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t5) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t5) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind b) u t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
end of H10
consider H10
we proved
<λ:T.Prop>
CASE THead (Bind b) u t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
eq T (THead (Bind Abbr) v2 t6) t4
→(pr0 v1 v2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
we proved
eq T (THead (Bind Abbr) v2 t6) t4
→(pr0 v1 v2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
by (previous H9 H6 H7)
we proved ty3 g c2 t4 (THead (Bind b) u t3)
∀H8:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t5)
THead (Bind b) u t2
.∀H9:(eq T (THead (Bind Abbr) v2 t6) t4).(ty3 g c2 t4 (THead (Bind b) u t3))
case pr0_upsilon b0:B H6:not (eq B b0 Abst) v1:T v2:T H7:pr0 v1 v2 u1:T u2:T H8:pr0 u1 u2 t5:T t6:T H9:pr0 t5 t6 ⇒
the thesis becomes
∀H10:eq
T
THead (Flat Appl) v1 (THead (Bind b0) u1 t5)
THead (Bind b) u t2
.∀H11:eq T (THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4
.ty3 g c2 t4 (THead (Bind b) u t3)
suppose H10:
eq
T
THead (Flat Appl) v1 (THead (Bind b0) u1 t5)
THead (Bind b) u t2
suppose H11: eq T (THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4
(H12)
we proceed by induction on H10 to prove
<λ:T.Prop>
CASE THead (Bind b) u t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind b0) u1 t5) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind b0) u1 t5) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind b) u t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
end of H12
consider H12
we proved
<λ:T.Prop>
CASE THead (Bind b) u t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
eq T (THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4
→(not (eq B b0 Abst)
→(pr0 v1 v2)→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
we proved
eq T (THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4
→(not (eq B b0 Abst)
→(pr0 v1 v2)→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
by (previous H11 H6 H7 H8 H9)
we proved ty3 g c2 t4 (THead (Bind b) u t3)
∀H10:eq
T
THead (Flat Appl) v1 (THead (Bind b0) u1 t5)
THead (Bind b) u t2
.∀H11:eq T (THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4
.ty3 g c2 t4 (THead (Bind b) u t3)
case pr0_delta u1:T u2:T H6:pr0 u1 u2 t5:T t6:T H7:pr0 t5 t6 w:T H8:subst0 O u2 t6 w ⇒
the thesis becomes
∀H9:eq T (THead (Bind Abbr) u1 t5) (THead (Bind b) u t2)
.∀H10:(eq T (THead (Bind Abbr) u2 w) t4).(ty3 g c2 t4 (THead (Bind b) u t3))
suppose H9: eq T (THead (Bind Abbr) u1 t5) (THead (Bind b) u t2)
suppose H10: eq T (THead (Bind Abbr) u2 w) t4
(H11)
by (f_equal . . . . . H9)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) u1 t5 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
<λ:T.T> CASE THead (Bind b) u t2 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
THead (Bind Abbr) u1 t5
λe:T.<λ:T.T> CASE e OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
THead (Bind b) u t2
end of H11
(h1)
(H12)
by (f_equal . . . . . H9)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) u1 t5 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
<λ:T.T> CASE THead (Bind b) u t2 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
THead (Bind Abbr) u1 t5
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
THead (Bind b) u t2
end of H12
(h1)
(H13)
by (f_equal . . . . . H9)
we proved
eq
B
<λ:T.B>
CASE THead (Bind Abbr) u1 t5 OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:T.B>
CASE THead (Bind b) u t2 OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
eq
B
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
THead (Bind Abbr) u1 t5
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
THead (Bind b) u t2
end of H13
consider H13
we proved
eq
B
<λ:T.B>
CASE THead (Bind Abbr) u1 t5 OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:T.B>
CASE THead (Bind b) u t2 OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
that is equivalent to eq B Abbr b
we proceed by induction on the previous result to prove
eq T u1 u
→(eq T t5 t2
→(eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind b) u t3))))
case refl_equal : ⇒
the thesis becomes
eq T u1 u
→(eq T t5 t2
→(eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3))))
suppose H14: eq T u1 u
by (sym_eq . . . H14)
we proved eq T u u1
we proceed by induction on the previous result to prove
eq T t5 t2
→(eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3)))
case refl_equal : ⇒
the thesis becomes
eq T t5 t2
→(eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3)))
suppose H15: eq T t5 t2
by (sym_eq . . . H15)
we proved eq T t2 t5
we proceed by induction on the previous result to prove
eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3))
case refl_equal : ⇒
the thesis becomes
eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u u2)→(pr0 t2 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3))
suppose H16: eq T (THead (Bind Abbr) u2 w) t4
we proceed by induction on H16 to prove (pr0 u u2)→(pr0 t2 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3))
case refl_equal : ⇒
the thesis becomes
pr0 u u2
→(pr0 t2 t6
→(subst0 O u2 t6 w)→(ty3 g c2 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u t3)))
suppose H17: pr0 u u2
suppose H18: pr0 t2 t6
suppose H19: subst0 O u2 t6 w
(H20)
consider H13
we proved
eq
B
<λ:T.B>
CASE THead (Bind Abbr) u1 t5 OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:T.B>
CASE THead (Bind b) u t2 OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
that is equivalent to eq B Abbr b
by (eq_ind_r . . . H3 . previous)
∀c3:C.(wcpr0 (CHead c (Bind Abbr) u) c3)→∀t7:T.(pr0 t2 t7)→(ty3 g c3 t7 t3)
end of H20
(h1)
by (pr0_refl .)
we proved pr0 u u
by (wcpr0_comp . . H4 . . previous .)
wcpr0 (CHead c (Bind Abbr) u) (CHead c2 (Bind Abbr) u)
end of h1
(h2) by (pr0_refl .) we proved pr0 t2 t2
by (H20 . h1 . h2)
we proved ty3 g (CHead c2 (Bind Abbr) u) t2 t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c2 (Bind Abbr) u) t3 t
we proceed by induction on the previous result to prove ty3 g c2 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u t3)
case ex_intro : x:T H22:ty3 g (CHead c2 (Bind Abbr) u) t3 x ⇒
the thesis becomes ty3 g c2 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u t3)
by (wcpr0_comp . . H4 . . H17 .)
we proved wcpr0 (CHead c (Bind Abbr) u) (CHead c2 (Bind Abbr) u2)
by (H20 . previous . H18)
we proved ty3 g (CHead c2 (Bind Abbr) u2) t6 t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c2 (Bind Abbr) u2) t3 t
we proceed by induction on the previous result to prove ty3 g c2 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u t3)
case ex_intro : x0:T :ty3 g (CHead c2 (Bind Abbr) u2) t3 x0 ⇒
the thesis becomes ty3 g c2 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u t3)
(h1)
by (pr0_refl .)
we proved pr0 u u
by (H1 . H4 . previous)
we proved ty3 g c2 u t0
by (ty3_bind . . . . previous . . . H22)
ty3 g c2 (THead (Bind Abbr) u t3) (THead (Bind Abbr) u x)
end of h1
(h2)
(h1) by (H1 . H4 . H17) we proved ty3 g c2 u2 t0
(h2)
(h1)
by (wcpr0_comp . . H4 . . H17 .)
we proved wcpr0 (CHead c (Bind Abbr) u) (CHead c2 (Bind Abbr) u2)
by (H20 . previous . H18)
ty3 g (CHead c2 (Bind Abbr) u2) t6 t3
end of h1
(h2)
by (getl_refl . . .)
getl O (CHead c2 (Bind Abbr) u2) (CHead c2 (Bind Abbr) u2)
end of h2
by (ty3_subst0 . . . . h1 . . . h2 . H19)
ty3 g (CHead c2 (Bind Abbr) u2) w t3
end of h2
by (ty3_bind . . . . h1 . . . h2)
ty3 g c2 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u2 t3)
end of h2
(h3)
by (pr2_free . . . H17)
we proved pr2 c2 u u2
by (pr2_head_1 . . . previous . .)
we proved pr2 c2 (THead (Bind Abbr) u t3) (THead (Bind Abbr) u2 t3)
by (pc3_pr2_x . . . previous)
pc3 c2 (THead (Bind Abbr) u2 t3) (THead (Bind Abbr) u t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c2 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u t3)
ty3 g c2 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u t3)
we proved ty3 g c2 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u t3)
pr0 u u2
→(pr0 t2 t6
→(subst0 O u2 t6 w)→(ty3 g c2 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u t3)))
we proved (pr0 u u2)→(pr0 t2 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3))
eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u u2)→(pr0 t2 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3))
we proved
eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3))
eq T t5 t2
→(eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3)))
we proved
eq T t5 t2
→(eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3)))
eq T u1 u
→(eq T t5 t2
→(eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind Abbr) u t3))))
eq T u1 u
→(eq T t5 t2
→(eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind b) u t3))))
end of h1
(h2)
consider H12
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) u1 t5 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
<λ:T.T> CASE THead (Bind b) u t2 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
eq T u1 u
end of h2
by (h1 h2)
eq T t5 t2
→(eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind b) u t3)))
end of h1
(h2)
consider H11
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) u1 t5 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
<λ:T.T> CASE THead (Bind b) u t2 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
eq T t5 t2
end of h2
by (h1 h2)
we proved
eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Bind b) u t3))
by (previous H10 H6 H7 H8)
we proved ty3 g c2 t4 (THead (Bind b) u t3)
∀H9:eq T (THead (Bind Abbr) u1 t5) (THead (Bind b) u t2)
.∀H10:(eq T (THead (Bind Abbr) u2 w) t4).(ty3 g c2 t4 (THead (Bind b) u t3))
case pr0_zeta b0:B H6:not (eq B b0 Abst) t5:T t6:T H7:pr0 t5 t6 u0:T ⇒
the thesis becomes
∀H8:eq T (THead (Bind b0) u0 (lift (S O) O t5)) (THead (Bind b) u t2)
.∀H9:(eq T t6 t4).(ty3 g c2 t4 (THead (Bind b) u t3))
suppose H8: eq T (THead (Bind b0) u0 (lift (S O) O t5)) (THead (Bind b) u t2)
suppose H9: eq T t6 t4
(H10)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T>
CASE THead (Bind b0) u0 (lift (S O) O t5) OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| THead t7⇒t7
<λ:T.T>
CASE THead (Bind b) u t2 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| THead t7⇒t7
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| THead t7⇒t7
THead (Bind b0) u0 (lift (S O) O t5)
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| THead t7⇒t7
THead (Bind b) u t2
end of H10
(h1)
(H11)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T>
CASE THead (Bind b0) u0 (lift (S O) O t5) OF
TSort ⇒u0
| TLRef ⇒u0
| THead t7 ⇒t7
<λ:T.T> CASE THead (Bind b) u t2 OF TSort ⇒u0 | TLRef ⇒u0 | THead t7 ⇒t7
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t7 ⇒t7
THead (Bind b0) u0 (lift (S O) O t5)
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t7 ⇒t7
THead (Bind b) u t2
end of H11
(h1)
(H12)
by (f_equal . . . . . H8)
we proved
eq
B
<λ:T.B>
CASE THead (Bind b0) u0 (lift (S O) O t5) OF
TSort ⇒b0
| TLRef ⇒b0
| THead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
<λ:T.B>
CASE THead (Bind b) u t2 OF
TSort ⇒b0
| TLRef ⇒b0
| THead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
eq
B
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒b0
| TLRef ⇒b0
| THead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
THead (Bind b0) u0 (lift (S O) O t5)
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒b0
| TLRef ⇒b0
| THead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
THead (Bind b) u t2
end of H12
consider H12
we proved
eq
B
<λ:T.B>
CASE THead (Bind b0) u0 (lift (S O) O t5) OF
TSort ⇒b0
| TLRef ⇒b0
| THead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
<λ:T.B>
CASE THead (Bind b) u t2 OF
TSort ⇒b0
| TLRef ⇒b0
| THead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
that is equivalent to eq B b0 b
by (sym_eq . . . previous)
we proved eq B b b0
we proceed by induction on the previous result to prove
eq T u0 u
→(eq T (lift (S O) O t5) t2
→(eq T t6 t4
→(not (eq B b0 Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))))
case refl_equal : ⇒
the thesis becomes
eq T u0 u
→(eq T (lift (S O) O t5) t2
→(eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))))
suppose H13: eq T u0 u
by (sym_eq . . . H13)
we proved eq T u u0
we proceed by induction on the previous result to prove
eq T (lift (S O) O t5) t2
→(eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
case refl_equal : ⇒
the thesis becomes
eq T (lift (S O) O t5) t2
→(eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
suppose H14: eq T (lift (S O) O t5) t2
we proceed by induction on H14 to prove
eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
case refl_equal : ⇒
the thesis becomes
eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
suppose H15: eq T t6 t4
by (sym_eq . . . H15)
we proved eq T t4 t6
we proceed by induction on the previous result to prove (not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
case refl_equal : ⇒
the thesis becomes (not (eq B b Abst))→(pr0 t5 t4)→(ty3 g c2 t4 (THead (Bind b) u t3))
suppose H16: not (eq B b Abst)
suppose H17: pr0 t5 t4
(H18)
by (eq_ind_r . . . H3 . H14)
∀c3:C.(wcpr0 (CHead c (Bind b) u) c3)→∀t8:T.(pr0 (lift (S O) O t5) t8)→(ty3 g c3 t8 t3)
end of H18
(h1)
by (pr0_refl .)
we proved pr0 u u
by (wcpr0_comp . . H4 . . previous .)
wcpr0 (CHead c (Bind b) u) (CHead c2 (Bind b) u)
end of h1
(h2)
by (pr0_lift . . H17 . .)
pr0 (lift (S O) O t5) (lift (S O) O t4)
end of h2
by (H18 . h1 . h2)
we proved ty3 g (CHead c2 (Bind b) u) (lift (S O) O t4) t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c2 (Bind b) u) t3 t
we proceed by induction on the previous result to prove ty3 g c2 t4 (THead (Bind b) u t3)
case ex_intro : x:T H20:ty3 g (CHead c2 (Bind b) u) t3 x ⇒
the thesis becomes ty3 g c2 t4 (THead (Bind b) u t3)
(h1)
by (pr0_refl .)
we proved pr0 u u
by (wcpr0_comp . . H4 . . previous .)
wcpr0 (CHead c (Bind b) u) (CHead c2 (Bind b) u)
end of h1
(h2)
by (pr0_lift . . H17 . .)
pr0 (lift (S O) O t5) (lift (S O) O t4)
end of h2
by (H18 . h1 . h2)
we proved ty3 g (CHead c2 (Bind b) u) (lift (S O) O t4) t3
suppose H21: not (eq B Abbr Abst)
suppose H22: ty3 g (CHead c2 (Bind Abbr) u) t3 x
suppose H23: ty3 g (CHead c2 (Bind Abbr) u) (lift (S O) O t4) t3
(H24)
(h1)
by (getl_refl . . .)
getl O (CHead c2 (Bind Abbr) u) (CHead c2 (Bind Abbr) u)
end of h1
(h2)
by (csubst1_refl . . .)
csubst1 O u (CHead c2 (Bind Abbr) u) (CHead c2 (Bind Abbr) u)
end of h2
(h3)
by (drop_refl .)
we proved drop O O c2 c2
that is equivalent to drop (r (Bind Abbr) O) O c2 c2
by (drop_drop . . . . previous .)
drop (S O) O (CHead c2 (Bind Abbr) u) c2
end of h3
by (ty3_gen_cabbr . . . . H23 . . . h1 . h2 . h3)
ex3_2
T
T
λy1:T.λ:T.subst1 O u (lift (S O) O t4) (lift (S O) O y1)
λ:T.λy2:T.subst1 O u t3 (lift (S O) O y2)
λy1:T.λy2:T.ty3 g c2 y1 y2
end of H24
we proceed by induction on H24 to prove ty3 g c2 t4 (THead (Bind Abbr) u t3)
case ex3_2_intro : x0:T x1:T H25:subst1 O u (lift (S O) O t4) (lift (S O) O x0) H26:subst1 O u t3 (lift (S O) O x1) H27:ty3 g c2 x0 x1 ⇒
the thesis becomes ty3 g c2 t4 (THead (Bind Abbr) u t3)
(H28)
(h1) by (le_n .) we proved le O O
(h2)
(h1)
by (le_n .)
we proved le (plus (S O) O) (plus (S O) O)
lt O (plus (S O) O)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus O (S O)) (plus (S O) O)
end of h2
by (eq_ind_r . . . h1 . h2)
lt O (plus O (S O))
end of h2
by (subst1_gen_lift_eq . . . . . . h1 h2 H25)
we proved eq T (lift (S O) O x0) (lift (S O) O t4)
by (lift_inj . . . . previous)
we proved eq T x0 t4
we proceed by induction on the previous result to prove ty3 g c2 t4 x1
case refl_equal : ⇒
the thesis becomes the hypothesis H27
ty3 g c2 t4 x1
end of H28
(h1)
by (pr0_refl .)
we proved pr0 u u
by (H1 . H4 . previous)
we proved ty3 g c2 u t0
by (ty3_bind . . . . previous . . . H22)
ty3 g c2 (THead (Bind Abbr) u t3) (THead (Bind Abbr) u x)
end of h1
(h2)
(h1)
(h1) by (pr0_refl .) we proved pr0 u u
(h2) by (pr0_refl .) we proved pr0 t3 t3
by (pr0_delta1 . . h1 . . h2 . H26)
we proved
pr0
THead (Bind Abbr) u t3
THead (Bind Abbr) u (lift (S O) O x1)
by (pr2_free . . . previous)
we proved
pr2
c2
THead (Bind Abbr) u t3
THead (Bind Abbr) u (lift (S O) O x1)
by (pr3_pr2 . . . previous)
pr3
c2
THead (Bind Abbr) u t3
THead (Bind Abbr) u (lift (S O) O x1)
end of h1
(h2)
by (pr0_refl .)
we proved pr0 x1 x1
by (pr0_zeta . H21 . . previous .)
we proved pr0 (THead (Bind Abbr) u (lift (S O) O x1)) x1
by (pr2_free . . . previous)
we proved pr2 c2 (THead (Bind Abbr) u (lift (S O) O x1)) x1
by (pr3_pr2 . . . previous)
pr3 c2 (THead (Bind Abbr) u (lift (S O) O x1)) x1
end of h2
by (pr3_t . . . h1 . h2)
we proved pr3 c2 (THead (Bind Abbr) u t3) x1
by (pc3_pr3_x . . . previous)
pc3 c2 x1 (THead (Bind Abbr) u t3)
end of h2
by (ty3_conv . . . . h1 . . H28 h2)
ty3 g c2 t4 (THead (Bind Abbr) u t3)
we proved ty3 g c2 t4 (THead (Bind Abbr) u t3)
not (eq B Abbr Abst)
→(ty3 g (CHead c2 (Bind Abbr) u) t3 x
→(ty3 g (CHead c2 (Bind Abbr) u) (lift (S O) O t4) t3
→ty3 g c2 t4 (THead (Bind Abbr) u t3)))
suppose H21: not (eq B Abst Abst)
suppose : ty3 g (CHead c2 (Bind Abst) u) t3 x
suppose : ty3 g (CHead c2 (Bind Abst) u) (lift (S O) O t4) t3
(H24)
by (refl_equal . .)
we proved eq B Abst Abst
by (H21 previous)
we proved False
by cases on the previous result we prove ty3 g c2 t4 (THead (Bind Abst) u t3)
ty3 g c2 t4 (THead (Bind Abst) u t3)
end of H24
consider H24
we proved ty3 g c2 t4 (THead (Bind Abst) u t3)
not (eq B Abst Abst)
→(ty3 g (CHead c2 (Bind Abst) u) t3 x
→(ty3 g (CHead c2 (Bind Abst) u) (lift (S O) O t4) t3
→ty3 g c2 t4 (THead (Bind Abst) u t3)))
suppose H21: not (eq B Void Abst)
suppose H22: ty3 g (CHead c2 (Bind Void) u) t3 x
suppose H23: ty3 g (CHead c2 (Bind Void) u) (lift (S O) O t4) t3
(H24)
(h1)
by (getl_refl . . .)
getl O (CHead c2 (Bind Void) u) (CHead c2 (Bind Void) u)
end of h1
(h2)
by (drop_refl .)
we proved drop O O c2 c2
that is equivalent to drop (r (Bind Void) O) O c2 c2
by (drop_drop . . . . previous .)
drop (S O) O (CHead c2 (Bind Void) u) c2
end of h2
by (ty3_gen_cvoid . . . . H23 . . . h1 . h2)
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) O t4) (lift (S O) O y1)
λ:T.λy2:T.eq T t3 (lift (S O) O y2)
λy1:T.λy2:T.ty3 g c2 y1 y2
end of H24
we proceed by induction on H24 to prove ty3 g c2 t4 (THead (Bind Void) u t3)
case ex3_2_intro : x0:T x1:T H25:eq T (lift (S O) O t4) (lift (S O) O x0) H26:eq T t3 (lift (S O) O x1) H27:ty3 g c2 x0 x1 ⇒
the thesis becomes ty3 g c2 t4 (THead (Bind Void) u t3)
(H28)
we proceed by induction on H26 to prove ty3 g (CHead c2 (Bind Void) u) (lift (S O) O x1) x
case refl_equal : ⇒
the thesis becomes the hypothesis H22
ty3 g (CHead c2 (Bind Void) u) (lift (S O) O x1) x
end of H28
(H29)
by (lift_inj . . . . H25)
we proved eq T t4 x0
by (eq_ind_r . . . H27 . previous)
ty3 g c2 t4 x1
end of H29
(h1)
by (pr0_refl .)
we proved pr0 u u
by (H1 . H4 . previous)
we proved ty3 g c2 u t0
by (ty3_bind . . . . previous . . . H28)
ty3
g
c2
THead (Bind Void) u (lift (S O) O x1)
THead (Bind Void) u x
end of h1
(h2)
by (pr0_refl .)
we proved pr0 x1 x1
by (pr0_zeta . H21 . . previous .)
we proved pr0 (THead (Bind Void) u (lift (S O) O x1)) x1
by (pr2_free . . . previous)
we proved pr2 c2 (THead (Bind Void) u (lift (S O) O x1)) x1
by (pc3_pr2_r . . . previous)
we proved pc3 c2 (THead (Bind Void) u (lift (S O) O x1)) x1
by (pc3_s . . . previous)
pc3 c2 x1 (THead (Bind Void) u (lift (S O) O x1))
end of h2
by (ty3_conv . . . . h1 . . H29 h2)
we proved ty3 g c2 t4 (THead (Bind Void) u (lift (S O) O x1))
by (eq_ind_r . . . previous . H26)
ty3 g c2 t4 (THead (Bind Void) u t3)
we proved ty3 g c2 t4 (THead (Bind Void) u t3)
not (eq B Void Abst)
→(ty3 g (CHead c2 (Bind Void) u) t3 x
→(ty3 g (CHead c2 (Bind Void) u) (lift (S O) O t4) t3
→ty3 g c2 t4 (THead (Bind Void) u t3)))
by (previous . H16 H20 previous)
ty3 g c2 t4 (THead (Bind b) u t3)
we proved ty3 g c2 t4 (THead (Bind b) u t3)
(not (eq B b Abst))→(pr0 t5 t4)→(ty3 g c2 t4 (THead (Bind b) u t3))
we proved (not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
we proved
eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
eq T (lift (S O) O t5) t2
→(eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
we proved
eq T (lift (S O) O t5) t2
→(eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
eq T u0 u
→(eq T (lift (S O) O t5) t2
→(eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))))
eq T u0 u
→(eq T (lift (S O) O t5) t2
→(eq T t6 t4
→(not (eq B b0 Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))))
end of h1
(h2)
consider H11
we proved
eq
T
<λ:T.T>
CASE THead (Bind b0) u0 (lift (S O) O t5) OF
TSort ⇒u0
| TLRef ⇒u0
| THead t7 ⇒t7
<λ:T.T> CASE THead (Bind b) u t2 OF TSort ⇒u0 | TLRef ⇒u0 | THead t7 ⇒t7
eq T u0 u
end of h2
by (h1 h2)
eq T (lift (S O) O t5) t2
→(eq T t6 t4
→(not (eq B b0 Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3)))
end of h1
(h2)
consider H10
we proved
eq
T
<λ:T.T>
CASE THead (Bind b0) u0 (lift (S O) O t5) OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| THead t7⇒t7
<λ:T.T>
CASE THead (Bind b) u t2 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt7:T
.<λt8:T.T>
CASE t7 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t8⇒THead k (lref_map f d u1) (lref_map f (s k d) t8)
}
λx:nat.plus x (S O)
O
t5
| THead t7⇒t7
eq T (lift (S O) O t5) t2
end of h2
by (h1 h2)
we proved
eq T t6 t4
→(not (eq B b0 Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
by (previous H9 H6 H7)
we proved ty3 g c2 t4 (THead (Bind b) u t3)
∀H8:eq T (THead (Bind b0) u0 (lift (S O) O t5)) (THead (Bind b) u t2)
.∀H9:(eq T t6 t4).(ty3 g c2 t4 (THead (Bind b) u t3))
case pr0_tau t5:T t6:T H6:pr0 t5 t6 u0:T ⇒
the thesis becomes
∀H7:eq T (THead (Flat Cast) u0 t5) (THead (Bind b) u t2)
.∀H8:(eq T t6 t4).(ty3 g c2 t4 (THead (Bind b) u t3))
suppose H7: eq T (THead (Flat Cast) u0 t5) (THead (Bind b) u t2)
suppose H8: eq T t6 t4
(H9)
we proceed by induction on H7 to prove
<λ:T.Prop>
CASE THead (Bind b) u t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Cast) u0 t5 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Cast) u0 t5 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind b) u t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
end of H9
consider H9
we proved
<λ:T.Prop>
CASE THead (Bind b) u t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove (eq T t6 t4)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
we proved (eq T t6 t4)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Bind b) u t3))
by (previous H8 H6)
we proved ty3 g c2 t4 (THead (Bind b) u t3)
∀H7:eq T (THead (Flat Cast) u0 t5) (THead (Bind b) u t2)
.∀H8:(eq T t6 t4).(ty3 g c2 t4 (THead (Bind b) u t3))
eq T (THead (Bind b) u t2) (THead (Bind b) u t2)
→(eq T t4 t4)→(ty3 g c2 t4 (THead (Bind b) u t3))
end of H6
(h1)
by (refl_equal . .)
eq T (THead (Bind b) u t2) (THead (Bind b) u t2)
end of h1
(h2)
by (refl_equal . .)
eq T t4 t4
end of h2
by (H6 h1 h2)
we proved ty3 g c2 t4 (THead (Bind b) u t3)
∀c2:C.∀H4:(wcpr0 c c2).∀t4:T.∀H5:(pr0 (THead (Bind b) u t2) t4).(ty3 g c2 t4 (THead (Bind b) u t3))
case ty3_appl : c:C w:T u:T :ty3 g c w u v:T t0:T H2:ty3 g c v (THead (Bind Abst) u t0) ⇒
the thesis becomes
∀c2:C
.∀H4:wcpr0 c c2
.∀t2:T
.∀H5:pr0 (THead (Flat Appl) w v) t2
.ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
(H1) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t2:T.(pr0 w t2)→(ty3 g c2 t2 u)
(H3) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t2:T.(pr0 v t2)→(ty3 g c2 t2 (THead (Bind Abst) u t0))
assume c2: C
suppose H4: wcpr0 c c2
assume t2: T
suppose H5: pr0 (THead (Flat Appl) w v) t2
(H6)
by cases on H5 we prove
eq T (THead (Flat Appl) w v) (THead (Flat Appl) w v)
→(eq T t2 t2)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
case pr0_refl t3:T ⇒
the thesis becomes
∀H6:eq T t3 (THead (Flat Appl) w v)
.∀H7:(eq T t3 t2).(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
suppose H6: eq T t3 (THead (Flat Appl) w v)
suppose H7: eq T t3 t2
by (sym_eq . . . H6)
we proved eq T (THead (Flat Appl) w v) t3
suppose H8: eq T (THead (Flat Appl) w v) t2
we proceed by induction on H8 to prove ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case refl_equal : ⇒
the thesis becomes
ty3
g
c2
THead (Flat Appl) w v
THead (Flat Appl) w (THead (Bind Abst) u t0)
(h1)
by (pr0_refl .)
we proved pr0 w w
by (H1 . H4 . previous)
ty3 g c2 w u
end of h1
(h2)
by (pr0_refl .)
we proved pr0 v v
by (H3 . H4 . previous)
ty3 g c2 v (THead (Bind Abst) u t0)
end of h2
by (ty3_appl . . . . h1 . . h2)
ty3
g
c2
THead (Flat Appl) w v
THead (Flat Appl) w (THead (Bind Abst) u t0)
we proved ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
eq T (THead (Flat Appl) w v) t2
→ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
by (previous previous H7)
we proved ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
∀H6:eq T t3 (THead (Flat Appl) w v)
.∀H7:(eq T t3 t2).(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
case pr0_comp u1:T u2:T H6:pr0 u1 u2 t3:T t4:T H7:pr0 t3 t4 k:K ⇒
the thesis becomes
∀H8:eq T (THead k u1 t3) (THead (Flat Appl) w v)
.∀H9:eq T (THead k u2 t4) t2
.ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
suppose H8: eq T (THead k u1 t3) (THead (Flat Appl) w v)
suppose H9: eq T (THead k u2 t4) t2
(H10)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t5⇒t5
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒t3 | TLRef ⇒t3 | THead t5⇒t5
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t5⇒t5 (THead k u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t5⇒t5
THead (Flat Appl) w v
end of H10
(h1)
(H11)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t5 ⇒t5
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒u1 | TLRef ⇒u1 | THead t5 ⇒t5
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t5 ⇒t5 (THead k u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t5 ⇒t5
THead (Flat Appl) w v
end of H11
(h1)
(H12)
by (f_equal . . . . . H8)
we proved
eq
K
<λ:T.K> CASE THead k u1 t3 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Flat Appl) w v OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0 (THead k u1 t3)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
THead (Flat Appl) w v
end of H12
consider H12
we proved
eq
K
<λ:T.K> CASE THead k u1 t3 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Flat Appl) w v OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
that is equivalent to eq K k (Flat Appl)
by (sym_eq . . . previous)
we proved eq K (Flat Appl) k
we proceed by induction on the previous result to prove
eq T u1 w
→(eq T t3 v
→(eq T (THead k u2 t4) t2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))
case refl_equal : ⇒
the thesis becomes
eq T u1 w
→(eq T t3 v
→(eq T (THead (Flat Appl) u2 t4) t2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))
suppose H13: eq T u1 w
by (sym_eq . . . H13)
we proved eq T w u1
we proceed by induction on the previous result to prove
eq T t3 v
→(eq T (THead (Flat Appl) u2 t4) t2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
case refl_equal : ⇒
the thesis becomes
eq T t3 v
→(eq T (THead (Flat Appl) u2 t4) t2
→(pr0 w u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
suppose H14: eq T t3 v
by (sym_eq . . . H14)
we proved eq T v t3
we proceed by induction on the previous result to prove
eq T (THead (Flat Appl) u2 t4) t2
→(pr0 w u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
case refl_equal : ⇒
the thesis becomes
eq T (THead (Flat Appl) u2 t4) t2
→(pr0 w u2
→(pr0 v t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
suppose H15: eq T (THead (Flat Appl) u2 t4) t2
we proceed by induction on H15 to prove
pr0 w u2
→(pr0 v t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
case refl_equal : ⇒
the thesis becomes
pr0 w u2
→(pr0 v t4
→(ty3
g
c2
THead (Flat Appl) u2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)))
suppose H16: pr0 w u2
suppose H17: pr0 v t4
by (pr0_refl .)
we proved pr0 v v
by (H3 . H4 . previous)
we proved ty3 g c2 v (THead (Bind Abst) u t0)
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c2 (THead (Bind Abst) u t0) t
we proceed by induction on the previous result to prove
ty3
g
c2
THead (Flat Appl) u2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex_intro : x:T H18:ty3 g c2 (THead (Bind Abst) u t0) x ⇒
the thesis becomes
ty3
g
c2
THead (Flat Appl) u2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (ty3_gen_bind . . . . . . H18)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c2 (THead (Bind Abst) u t2) x
λ:T.λt:T.ty3 g c2 u t
λt2:T.λ:T.ty3 g (CHead c2 (Bind Abst) u) t0 t2
we proceed by induction on the previous result to prove
ty3
g
c2
THead (Flat Appl) u2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex3_2_intro : x0:T x1:T :pc3 c2 (THead (Bind Abst) u x0) x H20:ty3 g c2 u x1 H21:ty3 g (CHead c2 (Bind Abst) u) t0 x0 ⇒
the thesis becomes
ty3
g
c2
THead (Flat Appl) u2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
(h1)
(h1)
by (pr0_refl .)
we proved pr0 w w
by (H1 . H4 . previous)
ty3 g c2 w u
end of h1
(h2)
by (ty3_bind . . . . H20 . . . H21)
ty3 g c2 (THead (Bind Abst) u t0) (THead (Bind Abst) u x0)
end of h2
by (ty3_appl . . . . h1 . . h2)
ty3
g
c2
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u x0)
end of h1
(h2)
(h1) by (H1 . H4 . H16) we proved ty3 g c2 u2 u
(h2)
by (H3 . H4 . H17)
ty3 g c2 t4 (THead (Bind Abst) u t0)
end of h2
by (ty3_appl . . . . h1 . . h2)
ty3
g
c2
THead (Flat Appl) u2 t4
THead (Flat Appl) u2 (THead (Bind Abst) u t0)
end of h2
(h3)
by (pr2_free . . . H16)
we proved pr2 c2 w u2
by (pr2_head_1 . . . previous . .)
we proved
pr2
c2
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) u2 (THead (Bind Abst) u t0)
by (pc3_pr2_x . . . previous)
pc3
c2
THead (Flat Appl) u2 (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u t0)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3
g
c2
THead (Flat Appl) u2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c2
THead (Flat Appl) u2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
we proved
ty3
g
c2
THead (Flat Appl) u2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
pr0 w u2
→(pr0 v t4
→(ty3
g
c2
THead (Flat Appl) u2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)))
we proved
pr0 w u2
→(pr0 v t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
eq T (THead (Flat Appl) u2 t4) t2
→(pr0 w u2
→(pr0 v t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
we proved
eq T (THead (Flat Appl) u2 t4) t2
→(pr0 w u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
eq T t3 v
→(eq T (THead (Flat Appl) u2 t4) t2
→(pr0 w u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
we proved
eq T t3 v
→(eq T (THead (Flat Appl) u2 t4) t2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
eq T u1 w
→(eq T t3 v
→(eq T (THead (Flat Appl) u2 t4) t2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))
eq T u1 w
→(eq T t3 v
→(eq T (THead k u2 t4) t2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))
end of h1
(h2)
consider H11
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t5 ⇒t5
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒u1 | TLRef ⇒u1 | THead t5 ⇒t5
eq T u1 w
end of h2
by (h1 h2)
eq T t3 v
→(eq T (THead k u2 t4) t2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
end of h1
(h2)
consider H10
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t5⇒t5
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒t3 | TLRef ⇒t3 | THead t5⇒t5
eq T t3 v
end of h2
by (h1 h2)
we proved
eq T (THead k u2 t4) t2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
by (previous H9 H6 H7)
we proved ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
∀H8:eq T (THead k u1 t3) (THead (Flat Appl) w v)
.∀H9:eq T (THead k u2 t4) t2
.ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case pr0_beta u0:T v1:T v2:T H6:pr0 v1 v2 t3:T t4:T H7:pr0 t3 t4 ⇒
the thesis becomes
∀H8:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Flat Appl) w v
.∀H9:eq T (THead (Bind Abbr) v2 t4) t2
.ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
suppose H8:
eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Flat Appl) w v
suppose H9: eq T (THead (Bind Abbr) v2 t4) t2
(H10)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t3) OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t5⇒t5
<λ:T.T>
CASE THead (Flat Appl) w v OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t5⇒t5
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t5⇒t5
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t5⇒t5
THead (Flat Appl) w v
end of H10
(h1)
(H11)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t3) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t5 ⇒t5
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒v1 | TLRef ⇒v1 | THead t5 ⇒t5
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t5 ⇒t5
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t5 ⇒t5
THead (Flat Appl) w v
end of H11
consider H11
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t3) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t5 ⇒t5
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒v1 | TLRef ⇒v1 | THead t5 ⇒t5
that is equivalent to eq T v1 w
by (sym_eq . . . previous)
we proved eq T w v1
we proceed by induction on the previous result to prove
eq T (THead (Bind Abst) u0 t3) v
→(eq T (THead (Bind Abbr) v2 t4) t2
→(pr0 v1 v2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
case refl_equal : ⇒
the thesis becomes
eq T (THead (Bind Abst) u0 t3) v
→(eq T (THead (Bind Abbr) v2 t4) t2
→(pr0 w v2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
suppose H12: eq T (THead (Bind Abst) u0 t3) v
we proceed by induction on H12 to prove
eq T (THead (Bind Abbr) v2 t4) t2
→(pr0 w v2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
case refl_equal : ⇒
the thesis becomes
eq T (THead (Bind Abbr) v2 t4) t2
→(pr0 w v2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
suppose H13: eq T (THead (Bind Abbr) v2 t4) t2
we proceed by induction on H13 to prove
pr0 w v2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
case refl_equal : ⇒
the thesis becomes
pr0 w v2
→(pr0 t3 t4
→(ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)))
suppose H14: pr0 w v2
suppose H15: pr0 t3 t4
(H16)
by (eq_ind_r . . . H3 . H12)
∀c3:C
.wcpr0 c c3
→∀t6:T.(pr0 (THead (Bind Abst) u0 t3) t6)→(ty3 g c3 t6 (THead (Bind Abst) u t0))
end of H16
by (pr0_refl .)
we proved pr0 (THead (Bind Abst) u0 t3) (THead (Bind Abst) u0 t3)
by (H16 . H4 . previous)
we proved ty3 g c2 (THead (Bind Abst) u0 t3) (THead (Bind Abst) u t0)
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c2 (THead (Bind Abst) u t0) t
we proceed by induction on the previous result to prove
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex_intro : x:T H18:ty3 g c2 (THead (Bind Abst) u t0) x ⇒
the thesis becomes
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (ty3_gen_bind . . . . . . H18)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c2 (THead (Bind Abst) u t2) x
λ:T.λt:T.ty3 g c2 u t
λt2:T.λ:T.ty3 g (CHead c2 (Bind Abst) u) t0 t2
we proceed by induction on the previous result to prove
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex3_2_intro : x0:T x1:T :pc3 c2 (THead (Bind Abst) u x0) x H20:ty3 g c2 u x1 H21:ty3 g (CHead c2 (Bind Abst) u) t0 x0 ⇒
the thesis becomes
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (pr0_refl .)
we proved pr0 u0 u0
by (pr0_comp . . previous . . H15 .)
we proved pr0 (THead (Bind Abst) u0 t3) (THead (Bind Abst) u0 t4)
by (H16 . H4 . previous)
we proved ty3 g c2 (THead (Bind Abst) u0 t4) (THead (Bind Abst) u t0)
by (ty3_gen_bind . . . . . . previous)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c2 (THead (Bind Abst) u0 t2) (THead (Bind Abst) u t0)
λ:T.λt:T.ty3 g c2 u0 t
λt2:T.λ:T.ty3 g (CHead c2 (Bind Abst) u0) t4 t2
we proceed by induction on the previous result to prove
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex3_2_intro : x2:T x3:T H22:pc3 c2 (THead (Bind Abst) u0 x2) (THead (Bind Abst) u t0) H23:ty3 g c2 u0 x3 H24:ty3 g (CHead c2 (Bind Abst) u0) t4 x2 ⇒
the thesis becomes
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (pc3_gen_abst . . . . . H22)
we proved land (pc3 c2 u0 u) ∀b:B.∀u:T.(pc3 (CHead c2 (Bind b) u) x2 t0)
we proceed by induction on the previous result to prove
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
case conj : H25:pc3 c2 u0 u H26:∀b:B.∀u1:T.(pc3 (CHead c2 (Bind b) u1) x2 t0) ⇒
the thesis becomes
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
(h1)
(h1)
by (pr0_refl .)
we proved pr0 w w
by (H1 . H4 . previous)
ty3 g c2 w u
end of h1
(h2)
by (ty3_bind . . . . H20 . . . H21)
ty3 g c2 (THead (Bind Abst) u t0) (THead (Bind Abst) u x0)
end of h2
by (ty3_appl . . . . h1 . . h2)
ty3
g
c2
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u x0)
end of h1
(h2)
(h1) by (H1 . H4 . H14) we proved ty3 g c2 v2 u
(h2)
(h1) by (H1 . H4 . H14) we proved ty3 g c2 v2 u
(h2) by (pc3_s . . . H25) we proved pc3 c2 u u0
by (ty3_conv . . . . H23 . . h1 h2)
we proved ty3 g c2 v2 u0
by (csubt_ty3_ld . . . . previous . . H24)
ty3 g (CHead c2 (Bind Abbr) v2) t4 x2
end of h2
by (ty3_bind . . . . h1 . . . h2)
ty3 g c2 (THead (Bind Abbr) v2 t4) (THead (Bind Abbr) v2 x2)
end of h2
(h3)
(h1)
by (H26 . .)
we proved pc3 (CHead c2 (Bind Abbr) v2) x2 t0
by (pc3_head_2 . . . . . previous)
pc3 c2 (THead (Bind Abbr) v2 x2) (THead (Bind Abbr) v2 t0)
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t0 t0
by (pr0_beta . . . H14 . . previous)
we proved
pr0
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Bind Abbr) v2 t0
by (pr2_free . . . previous)
we proved
pr2
c2
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Bind Abbr) v2 t0
by (pc3_pr2_x . . . previous)
pc3
c2
THead (Bind Abbr) v2 t0
THead (Flat Appl) w (THead (Bind Abst) u t0)
end of h2
by (pc3_t . . . h1 . h2)
pc3
c2
THead (Bind Abbr) v2 x2
THead (Flat Appl) w (THead (Bind Abst) u t0)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
we proved
ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)
pr0 w v2
→(pr0 t3 t4
→(ty3
g
c2
THead (Bind Abbr) v2 t4
THead (Flat Appl) w (THead (Bind Abst) u t0)))
we proved
pr0 w v2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
eq T (THead (Bind Abbr) v2 t4) t2
→(pr0 w v2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
we proved
eq T (THead (Bind Abbr) v2 t4) t2
→(pr0 w v2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
eq T (THead (Bind Abst) u0 t3) v
→(eq T (THead (Bind Abbr) v2 t4) t2
→(pr0 w v2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
eq T (THead (Bind Abst) u0 t3) v
→(eq T (THead (Bind Abbr) v2 t4) t2
→(pr0 v1 v2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
end of h1
(h2)
consider H10
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t3) OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t5⇒t5
<λ:T.T>
CASE THead (Flat Appl) w v OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t5⇒t5
eq T (THead (Bind Abst) u0 t3) v
end of h2
by (h1 h2)
we proved
eq T (THead (Bind Abbr) v2 t4) t2
→(pr0 v1 v2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
by (previous H9 H6 H7)
we proved ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
∀H8:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Flat Appl) w v
.∀H9:eq T (THead (Bind Abbr) v2 t4) t2
.ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case pr0_upsilon b:B H6:not (eq B b Abst) v1:T v2:T H7:pr0 v1 v2 u1:T u2:T H8:pr0 u1 u2 t3:T t4:T H9:pr0 t3 t4 ⇒
the thesis becomes
∀H10:eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Flat Appl) w v
.∀H11:eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
.ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
suppose H10:
eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Flat Appl) w v
suppose H11: eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
(H12)
by (f_equal . . . . . H10)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t3) OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t5⇒t5
<λ:T.T>
CASE THead (Flat Appl) w v OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t5⇒t5
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t5⇒t5
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t5⇒t5
THead (Flat Appl) w v
end of H12
(h1)
(H13)
by (f_equal . . . . . H10)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t3) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t5 ⇒t5
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒v1 | TLRef ⇒v1 | THead t5 ⇒t5
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t5 ⇒t5
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t5 ⇒t5
THead (Flat Appl) w v
end of H13
consider H13
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t3) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t5 ⇒t5
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒v1 | TLRef ⇒v1 | THead t5 ⇒t5
that is equivalent to eq T v1 w
by (sym_eq . . . previous)
we proved eq T w v1
we proceed by induction on the previous result to prove
eq T (THead (Bind b) u1 t3) v
→(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
→(not (eq B b Abst)
→(pr0 v1 v2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))))
case refl_equal : ⇒
the thesis becomes
eq T (THead (Bind b) u1 t3) v
→(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
→(not (eq B b Abst)
→(pr0 w v2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))))
suppose H14: eq T (THead (Bind b) u1 t3) v
we proceed by induction on H14 to prove
eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
→(not (eq B b Abst)
→(pr0 w v2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))
case refl_equal : ⇒
the thesis becomes
eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
→(not (eq B b Abst)
→(pr0 w v2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))
suppose H15: eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
we proceed by induction on H15 to prove
not (eq B b Abst)
→(pr0 w v2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
case refl_equal : ⇒
the thesis becomes
not (eq B b Abst)
→(pr0 w v2
→(pr0 u1 u2
→(pr0 t3 t4
→(ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)))))
suppose H16: not (eq B b Abst)
suppose H17: pr0 w v2
suppose H18: pr0 u1 u2
suppose H19: pr0 t3 t4
(H20)
by (eq_ind_r . . . H3 . H14)
∀c3:C
.wcpr0 c c3
→∀t6:T.(pr0 (THead (Bind b) u1 t3) t6)→(ty3 g c3 t6 (THead (Bind Abst) u t0))
end of H20
by (pr0_comp . . H18 . . H19 .)
we proved pr0 (THead (Bind b) u1 t3) (THead (Bind b) u2 t4)
by (H20 . H4 . previous)
we proved ty3 g c2 (THead (Bind b) u2 t4) (THead (Bind Abst) u t0)
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c2 (THead (Bind Abst) u t0) t
we proceed by induction on the previous result to prove
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex_intro : x:T H22:ty3 g c2 (THead (Bind Abst) u t0) x ⇒
the thesis becomes
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
(H23) consider H22
by (ty3_gen_bind . . . . . . H23)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c2 (THead (Bind Abst) u t2) x
λ:T.λt:T.ty3 g c2 u t
λt2:T.λ:T.ty3 g (CHead c2 (Bind Abst) u) t0 t2
we proceed by induction on the previous result to prove
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex3_2_intro : x0:T x1:T :pc3 c2 (THead (Bind Abst) u x0) x H25:ty3 g c2 u x1 H26:ty3 g (CHead c2 (Bind Abst) u) t0 x0 ⇒
the thesis becomes
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (pr0_comp . . H18 . . H19 .)
we proved pr0 (THead (Bind b) u1 t3) (THead (Bind b) u2 t4)
by (H20 . H4 . previous)
we proved ty3 g c2 (THead (Bind b) u2 t4) (THead (Bind Abst) u t0)
by (ty3_gen_bind . . . . . . previous)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c2 (THead (Bind b) u2 t2) (THead (Bind Abst) u t0)
λ:T.λt:T.ty3 g c2 u2 t
λt2:T.λ:T.ty3 g (CHead c2 (Bind b) u2) t4 t2
we proceed by induction on the previous result to prove
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex3_2_intro : x2:T x3:T H27:pc3 c2 (THead (Bind b) u2 x2) (THead (Bind Abst) u t0) H28:ty3 g c2 u2 x3 H29:ty3 g (CHead c2 (Bind b) u2) t4 x2 ⇒
the thesis becomes
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
(H30)
by (lift_bind . . . . .)
we proved
eq
T
lift (S O) O (THead (Bind Abst) u t0)
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
we proceed by induction on the previous result to prove
pc3
CHead c2 (Bind b) u2
x2
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
case refl_equal : ⇒
the thesis becomes pc3 (CHead c2 (Bind b) u2) x2 (lift (S O) O (THead (Bind Abst) u t0))
by (pc3_gen_not_abst . H16 . . . . . H27)
pc3 (CHead c2 (Bind b) u2) x2 (lift (S O) O (THead (Bind Abst) u t0))
pc3
CHead c2 (Bind b) u2
x2
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
end of H30
(H31)
by (lift_bind . . . . .)
we proved
eq
T
lift (S O) O (THead (Bind Abst) u t0)
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
we proceed by induction on the previous result to prove
ty3
g
CHead c2 (Bind b) u2
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
lift (S O) O x
case refl_equal : ⇒
the thesis becomes
ty3
g
CHead c2 (Bind b) u2
lift (S O) O (THead (Bind Abst) u t0)
lift (S O) O x
by (drop_refl .)
we proved drop O O c2 c2
that is equivalent to drop (r (Bind b) O) O c2 c2
by (drop_drop . . . . previous .)
we proved drop (S O) O (CHead c2 (Bind b) u2) c2
by (ty3_lift . . . . H22 . . . previous)
ty3
g
CHead c2 (Bind b) u2
lift (S O) O (THead (Bind Abst) u t0)
lift (S O) O x
ty3
g
CHead c2 (Bind b) u2
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
lift (S O) O x
end of H31
by (ty3_gen_bind . . . . . . H31)
we proved
ex3_2
T
T
λt2:T
.λ:T
.pc3
CHead c2 (Bind b) u2
THead (Bind Abst) (lift (S O) O u) t2
lift (S O) O x
λ:T.λt:T.ty3 g (CHead c2 (Bind b) u2) (lift (S O) O u) t
λt2:T
.λ:T
.ty3
g
CHead (CHead c2 (Bind b) u2) (Bind Abst) (lift (S O) O u)
lift (S O) (S O) t0
t2
we proceed by induction on the previous result to prove
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex3_2_intro : x4:T x5:T :pc3 (CHead c2 (Bind b) u2) (THead (Bind Abst) (lift (S O) O u) x4) (lift (S O) O x) H33:ty3 g (CHead c2 (Bind b) u2) (lift (S O) O u) x5 H34:ty3 g (CHead (CHead c2 (Bind b) u2) (Bind Abst) (lift (S O) O u)) (lift (S O) (S O) t0) x4 ⇒
the thesis becomes
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
(h1)
(h1)
by (pr0_refl .)
we proved pr0 w w
by (H1 . H4 . previous)
ty3 g c2 w u
end of h1
(h2)
by (ty3_bind . . . . H25 . . . H26)
ty3 g c2 (THead (Bind Abst) u t0) (THead (Bind Abst) u x0)
end of h2
by (ty3_appl . . . . h1 . . h2)
ty3
g
c2
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u x0)
end of h1
(h2)
(h1)
(h1) by (H1 . H4 . H17) we proved ty3 g c2 v2 u
(h2)
by (drop_refl .)
we proved drop O O c2 c2
that is equivalent to drop (r (Bind b) O) O c2 c2
by (drop_drop . . . . previous .)
drop (S O) O (CHead c2 (Bind b) u2) c2
end of h2
by (ty3_lift . . . . h1 . . . h2)
ty3 g (CHead c2 (Bind b) u2) (lift (S O) O v2) (lift (S O) O u)
end of h1
(h2)
by (ty3_bind . . . . H33 . . . H34)
we proved
ty3
g
CHead c2 (Bind b) u2
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
THead (Bind Abst) (lift (S O) O u) x4
by (ty3_conv . . . . previous . . H29 H30)
ty3
g
CHead c2 (Bind b) u2
t4
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
end of h2
by (ty3_appl . . . . h1 . . h2)
we proved
ty3
g
CHead c2 (Bind b) u2
THead (Flat Appl) (lift (S O) O v2) t4
THead
Flat Appl
lift (S O) O v2
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
by (ty3_bind . . . . H28 . . . previous)
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead
Bind b
u2
THead
Flat Appl
lift (S O) O v2
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
end of h2
(h3)
by (lift_bind . . . . .)
we proved
eq
T
lift (S O) O (THead (Bind Abst) u t0)
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
we proceed by induction on the previous result to prove
pc3
c2
THead
Bind b
u2
THead
Flat Appl
lift (S O) O v2
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
THead (Flat Appl) w (THead (Bind Abst) u t0)
case refl_equal : ⇒
the thesis becomes
pc3
c2
THead
Bind b
u2
THead
Flat Appl
lift (S O) O v2
lift (S O) O (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u t0)
(h1)
(h1) by (pr0_refl .) we proved pr0 v2 v2
(h2) by (pr0_refl .) we proved pr0 u2 u2
(h3)
by (pr0_refl .)
pr0
lift (S O) O (THead (Bind Abst) u t0)
lift (S O) O (THead (Bind Abst) u t0)
end of h3
by (pr0_upsilon . H16 . . h1 . . h2 . . h3)
pr0
THead
Flat Appl
v2
THead (Bind b) u2 (lift (S O) O (THead (Bind Abst) u t0))
THead
Bind b
u2
THead
Flat Appl
lift (S O) O v2
lift (S O) O (THead (Bind Abst) u t0)
end of h1
(h2)
(h1)
by (pc1_pr0_x . . H17)
pc1 v2 w
end of h1
(h2)
by (pr0_refl .)
we proved pr0 (THead (Bind Abst) u t0) (THead (Bind Abst) u t0)
by (pr0_zeta . H16 . . previous .)
we proved
pr0
THead (Bind b) u2 (lift (S O) O (THead (Bind Abst) u t0))
THead (Bind Abst) u t0
by (pc1_pr0_r . . previous)
pc1
THead (Bind b) u2 (lift (S O) O (THead (Bind Abst) u t0))
THead (Bind Abst) u t0
end of h2
by (pc1_head . . h1 . . h2 .)
pc1
THead
Flat Appl
v2
THead (Bind b) u2 (lift (S O) O (THead (Bind Abst) u t0))
THead (Flat Appl) w (THead (Bind Abst) u t0)
end of h2
by (pc1_pr0_u2 . . h1 . h2)
we proved
pc1
THead
Bind b
u2
THead
Flat Appl
lift (S O) O v2
lift (S O) O (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (pc3_pc1 . . previous .)
pc3
c2
THead
Bind b
u2
THead
Flat Appl
lift (S O) O v2
lift (S O) O (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u t0)
pc3
c2
THead
Bind b
u2
THead
Flat Appl
lift (S O) O v2
THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)
THead (Flat Appl) w (THead (Bind Abst) u t0)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
we proved
ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)
not (eq B b Abst)
→(pr0 w v2
→(pr0 u1 u2
→(pr0 t3 t4
→(ty3
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
THead (Flat Appl) w (THead (Bind Abst) u t0)))))
we proved
not (eq B b Abst)
→(pr0 w v2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
→(not (eq B b Abst)
→(pr0 w v2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))
we proved
eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
→(not (eq B b Abst)
→(pr0 w v2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))
eq T (THead (Bind b) u1 t3) v
→(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
→(not (eq B b Abst)
→(pr0 w v2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))))
eq T (THead (Bind b) u1 t3) v
→(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
→(not (eq B b Abst)
→(pr0 v1 v2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))))
end of h1
(h2)
consider H12
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t3) OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t5⇒t5
<λ:T.T>
CASE THead (Flat Appl) w v OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t5⇒t5
eq T (THead (Bind b) u1 t3) v
end of h2
by (h1 h2)
we proved
eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
→(not (eq B b Abst)
→(pr0 v1 v2
→(pr0 u1 u2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))
by (previous H11 H6 H7 H8 H9)
we proved ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
∀H10:eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Flat Appl) w v
.∀H11:eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2
.ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case pr0_delta u1:T u2:T H6:pr0 u1 u2 t3:T t4:T H7:pr0 t3 t4 w0:T H8:subst0 O u2 t4 w0 ⇒
the thesis becomes
∀H9:eq T (THead (Bind Abbr) u1 t3) (THead (Flat Appl) w v)
.∀H10:eq T (THead (Bind Abbr) u2 w0) t2
.ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
suppose H9: eq T (THead (Bind Abbr) u1 t3) (THead (Flat Appl) w v)
suppose H10: eq T (THead (Bind Abbr) u2 w0) t2
(H11)
we proceed by induction on H9 to prove
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind Abbr) u1 t3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind Abbr) u1 t3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
end of H11
consider H11
we proved
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
eq T (THead (Bind Abbr) u2 w0) t2
→(pr0 u1 u2
→(pr0 t3 t4
→(subst0 O u2 t4 w0)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
we proved
eq T (THead (Bind Abbr) u2 w0) t2
→(pr0 u1 u2
→(pr0 t3 t4
→(subst0 O u2 t4 w0)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
by (previous H10 H6 H7 H8)
we proved ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
∀H9:eq T (THead (Bind Abbr) u1 t3) (THead (Flat Appl) w v)
.∀H10:eq T (THead (Bind Abbr) u2 w0) t2
.ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case pr0_zeta b:B H6:not (eq B b Abst) t3:T t4:T H7:pr0 t3 t4 u0:T ⇒
the thesis becomes
∀H8:eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Flat Appl) w v
.∀H9:(eq T t4 t2).(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
suppose H8:
eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Flat Appl) w v
suppose H9: eq T t4 t2
(H10)
we proceed by induction on H8 to prove
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind b) u0 (lift (S O) O t3) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) u0 (lift (S O) O t3) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
end of H10
consider H10
we proved
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
eq T t4 t2
→(not (eq B b Abst)
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
we proved
eq T t4 t2
→(not (eq B b Abst)
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
by (previous H9 H6 H7)
we proved ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
∀H8:eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Flat Appl) w v
.∀H9:(eq T t4 t2).(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
case pr0_tau t3:T t4:T H6:pr0 t3 t4 u0:T ⇒
the thesis becomes
∀H7:eq T (THead (Flat Cast) u0 t3) (THead (Flat Appl) w v)
.∀H8:(eq T t4 t2).(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
suppose H7: eq T (THead (Flat Cast) u0 t3) (THead (Flat Appl) w v)
suppose H8: eq T t4 t2
(H9)
we proceed by induction on H7 to prove
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Cast) u0 t3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Cast) u0 t3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
end of H9
consider H9
we proved
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
eq T t4 t2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
we proved
eq T t4 t2
→(pr0 t3 t4)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
by (previous H8 H6)
we proved ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
∀H7:eq T (THead (Flat Cast) u0 t3) (THead (Flat Appl) w v)
.∀H8:(eq T t4 t2).(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
eq T (THead (Flat Appl) w v) (THead (Flat Appl) w v)
→(eq T t2 t2)→(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))
end of H6
(h1)
by (refl_equal . .)
eq T (THead (Flat Appl) w v) (THead (Flat Appl) w v)
end of h1
(h2)
by (refl_equal . .)
eq T t2 t2
end of h2
by (H6 h1 h2)
we proved ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
∀c2:C
.∀H4:wcpr0 c c2
.∀t2:T
.∀H5:pr0 (THead (Flat Appl) w v) t2
.ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case ty3_cast : c:C t2:T t3:T :ty3 g c t2 t3 t0:T :ty3 g c t3 t0 ⇒
the thesis becomes ∀c2:C.∀H4:(wcpr0 c c2).∀t4:T.∀H5:(pr0 (THead (Flat Cast) t3 t2) t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
(H1) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t4:T.(pr0 t2 t4)→(ty3 g c2 t4 t3)
(H3) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t4:T.(pr0 t3 t4)→(ty3 g c2 t4 t0)
assume c2: C
suppose H4: wcpr0 c c2
assume t4: T
suppose H5: pr0 (THead (Flat Cast) t3 t2) t4
(H6)
by cases on H5 we prove
eq T (THead (Flat Cast) t3 t2) (THead (Flat Cast) t3 t2)
→(eq T t4 t4)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
case pr0_refl t5:T ⇒
the thesis becomes ∀H6:(eq T t5 (THead (Flat Cast) t3 t2)).∀H7:(eq T t5 t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
suppose H6: eq T t5 (THead (Flat Cast) t3 t2)
suppose H7: eq T t5 t4
by (sym_eq . . . H6)
we proved eq T (THead (Flat Cast) t3 t2) t5
suppose H8: eq T (THead (Flat Cast) t3 t2) t4
we proceed by induction on H8 to prove ty3 g c2 t4 (THead (Flat Cast) t0 t3)
case refl_equal : ⇒
the thesis becomes ty3 g c2 (THead (Flat Cast) t3 t2) (THead (Flat Cast) t0 t3)
(h1)
by (pr0_refl .)
we proved pr0 t2 t2
by (H1 . H4 . previous)
ty3 g c2 t2 t3
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t3 t3
by (H3 . H4 . previous)
ty3 g c2 t3 t0
end of h2
by (ty3_cast . . . . h1 . h2)
ty3 g c2 (THead (Flat Cast) t3 t2) (THead (Flat Cast) t0 t3)
we proved ty3 g c2 t4 (THead (Flat Cast) t0 t3)
(eq T (THead (Flat Cast) t3 t2) t4)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
by (previous previous H7)
we proved ty3 g c2 t4 (THead (Flat Cast) t0 t3)
∀H6:(eq T t5 (THead (Flat Cast) t3 t2)).∀H7:(eq T t5 t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
case pr0_comp u1:T u2:T H6:pr0 u1 u2 t5:T t6:T H7:pr0 t5 t6 k:K ⇒
the thesis becomes
∀H8:eq T (THead k u1 t5) (THead (Flat Cast) t3 t2)
.∀H9:(eq T (THead k u2 t6) t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
suppose H8: eq T (THead k u1 t5) (THead (Flat Cast) t3 t2)
suppose H9: eq T (THead k u2 t6) t4
(H10)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead k u1 t5 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
<λ:T.T> CASE THead (Flat Cast) t3 t2 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7 (THead k u1 t5)
λe:T.<λ:T.T> CASE e OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
THead (Flat Cast) t3 t2
end of H10
(h1)
(H11)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead k u1 t5 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
<λ:T.T> CASE THead (Flat Cast) t3 t2 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7 (THead k u1 t5)
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
THead (Flat Cast) t3 t2
end of H11
(h1)
(H12)
by (f_equal . . . . . H8)
we proved
eq
K
<λ:T.K> CASE THead k u1 t5 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K> CASE THead (Flat Cast) t3 t2 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0 (THead k u1 t5)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
THead (Flat Cast) t3 t2
end of H12
consider H12
we proved
eq
K
<λ:T.K> CASE THead k u1 t5 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K> CASE THead (Flat Cast) t3 t2 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
that is equivalent to eq K k (Flat Cast)
by (sym_eq . . . previous)
we proved eq K (Flat Cast) k
we proceed by induction on the previous result to prove
eq T u1 t3
→(eq T t5 t2
→(eq T (THead k u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))))
case refl_equal : ⇒
the thesis becomes
eq T u1 t3
→(eq T t5 t2
→(eq T (THead (Flat Cast) u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))))
suppose H13: eq T u1 t3
by (sym_eq . . . H13)
we proved eq T t3 u1
we proceed by induction on the previous result to prove
eq T t5 t2
→(eq T (THead (Flat Cast) u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3)))
case refl_equal : ⇒
the thesis becomes
eq T t5 t2
→(eq T (THead (Flat Cast) u2 t6) t4
→(pr0 t3 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3)))
suppose H14: eq T t5 t2
by (sym_eq . . . H14)
we proved eq T t2 t5
we proceed by induction on the previous result to prove
eq T (THead (Flat Cast) u2 t6) t4
→(pr0 t3 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
case refl_equal : ⇒
the thesis becomes
eq T (THead (Flat Cast) u2 t6) t4
→(pr0 t3 u2)→(pr0 t2 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
suppose H15: eq T (THead (Flat Cast) u2 t6) t4
we proceed by induction on H15 to prove (pr0 t3 u2)→(pr0 t2 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
case refl_equal : ⇒
the thesis becomes
pr0 t3 u2
→(pr0 t2 t6)→(ty3 g c2 (THead (Flat Cast) u2 t6) (THead (Flat Cast) t0 t3))
suppose H16: pr0 t3 u2
suppose H17: pr0 t2 t6
by (pr0_refl .)
we proved pr0 t3 t3
by (H3 . H4 . previous)
we proved ty3 g c2 t3 t0
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c2 t0 t
we proceed by induction on the previous result to prove ty3 g c2 (THead (Flat Cast) u2 t6) (THead (Flat Cast) t0 t3)
case ex_intro : x:T H18:ty3 g c2 t0 x ⇒
the thesis becomes ty3 g c2 (THead (Flat Cast) u2 t6) (THead (Flat Cast) t0 t3)
(h1)
by (pr0_refl .)
we proved pr0 t3 t3
by (H3 . H4 . previous)
we proved ty3 g c2 t3 t0
by (ty3_cast . . . . previous . H18)
ty3 g c2 (THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0)
end of h1
(h2)
(h1)
(h1) by (H3 . H4 . H16) we proved ty3 g c2 u2 t0
(h2) by (H1 . H4 . H17) we proved ty3 g c2 t6 t3
(h3)
by (pr2_free . . . H16)
we proved pr2 c2 t3 u2
by (pc3_pr2_r . . . previous)
pc3 c2 t3 u2
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c2 t6 u2
end of h1
(h2) by (H3 . H4 . H16) we proved ty3 g c2 u2 t0
by (ty3_cast . . . . h1 . h2)
ty3 g c2 (THead (Flat Cast) u2 t6) (THead (Flat Cast) t0 u2)
end of h2
(h3)
by (pr2_free . . . H16)
we proved pr2 c2 t3 u2
by (pr2_thin_dx . . . previous . .)
we proved pr2 c2 (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 u2)
by (pc3_pr2_r . . . previous)
we proved pc3 c2 (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 u2)
by (pc3_s . . . previous)
pc3 c2 (THead (Flat Cast) t0 u2) (THead (Flat Cast) t0 t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c2 (THead (Flat Cast) u2 t6) (THead (Flat Cast) t0 t3)
we proved ty3 g c2 (THead (Flat Cast) u2 t6) (THead (Flat Cast) t0 t3)
pr0 t3 u2
→(pr0 t2 t6)→(ty3 g c2 (THead (Flat Cast) u2 t6) (THead (Flat Cast) t0 t3))
we proved (pr0 t3 u2)→(pr0 t2 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
eq T (THead (Flat Cast) u2 t6) t4
→(pr0 t3 u2)→(pr0 t2 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
we proved
eq T (THead (Flat Cast) u2 t6) t4
→(pr0 t3 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
eq T t5 t2
→(eq T (THead (Flat Cast) u2 t6) t4
→(pr0 t3 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3)))
we proved
eq T t5 t2
→(eq T (THead (Flat Cast) u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3)))
eq T u1 t3
→(eq T t5 t2
→(eq T (THead (Flat Cast) u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))))
eq T u1 t3
→(eq T t5 t2
→(eq T (THead k u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))))
end of h1
(h2)
consider H11
we proved
eq
T
<λ:T.T> CASE THead k u1 t5 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
<λ:T.T> CASE THead (Flat Cast) t3 t2 OF TSort ⇒u1 | TLRef ⇒u1 | THead t7 ⇒t7
eq T u1 t3
end of h2
by (h1 h2)
eq T t5 t2
→(eq T (THead k u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3)))
end of h1
(h2)
consider H10
we proved
eq
T
<λ:T.T> CASE THead k u1 t5 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
<λ:T.T> CASE THead (Flat Cast) t3 t2 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
eq T t5 t2
end of h2
by (h1 h2)
we proved
eq T (THead k u2 t6) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
by (previous H9 H6 H7)
we proved ty3 g c2 t4 (THead (Flat Cast) t0 t3)
∀H8:eq T (THead k u1 t5) (THead (Flat Cast) t3 t2)
.∀H9:(eq T (THead k u2 t6) t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
case pr0_beta u:T v1:T v2:T H6:pr0 v1 v2 t5:T t6:T H7:pr0 t5 t6 ⇒
the thesis becomes
∀H8:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u t5)
THead (Flat Cast) t3 t2
.∀H9:(eq T (THead (Bind Abbr) v2 t6) t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
suppose H8:
eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u t5)
THead (Flat Cast) t3 t2
suppose H9: eq T (THead (Bind Abbr) v2 t6) t4
(H10)
we proceed by induction on H8 to prove
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u t5) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u t5) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
end of H10
consider H10
we proved
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
eq T (THead (Bind Abbr) v2 t6) t4
→(pr0 v1 v2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
we proved
eq T (THead (Bind Abbr) v2 t6) t4
→(pr0 v1 v2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
by (previous H9 H6 H7)
we proved ty3 g c2 t4 (THead (Flat Cast) t0 t3)
∀H8:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u t5)
THead (Flat Cast) t3 t2
.∀H9:(eq T (THead (Bind Abbr) v2 t6) t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
case pr0_upsilon b:B H6:not (eq B b Abst) v1:T v2:T H7:pr0 v1 v2 u1:T u2:T H8:pr0 u1 u2 t5:T t6:T H9:pr0 t5 t6 ⇒
the thesis becomes
∀H10:eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t5)
THead (Flat Cast) t3 t2
.∀H11:eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4
.ty3 g c2 t4 (THead (Flat Cast) t0 t3)
suppose H10:
eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t5)
THead (Flat Cast) t3 t2
suppose H11: eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4
(H12)
we proceed by induction on H10 to prove
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t5) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t5) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
end of H12
consider H12
we proved
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4
→(not (eq B b Abst)
→(pr0 v1 v2)→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3)))
we proved
eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4
→(not (eq B b Abst)
→(pr0 v1 v2)→(pr0 u1 u2)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3)))
by (previous H11 H6 H7 H8 H9)
we proved ty3 g c2 t4 (THead (Flat Cast) t0 t3)
∀H10:eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t5)
THead (Flat Cast) t3 t2
.∀H11:eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4
.ty3 g c2 t4 (THead (Flat Cast) t0 t3)
case pr0_delta u1:T u2:T H6:pr0 u1 u2 t5:T t6:T H7:pr0 t5 t6 w:T H8:subst0 O u2 t6 w ⇒
the thesis becomes
∀H9:eq T (THead (Bind Abbr) u1 t5) (THead (Flat Cast) t3 t2)
.∀H10:(eq T (THead (Bind Abbr) u2 w) t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
suppose H9: eq T (THead (Bind Abbr) u1 t5) (THead (Flat Cast) t3 t2)
suppose H10: eq T (THead (Bind Abbr) u2 w) t4
(H11)
we proceed by induction on H9 to prove
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind Abbr) u1 t5 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind Abbr) u1 t5 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
end of H11
consider H11
we proved
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
we proved
eq T (THead (Bind Abbr) u2 w) t4
→(pr0 u1 u2)→(pr0 t5 t6)→(subst0 O u2 t6 w)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
by (previous H10 H6 H7 H8)
we proved ty3 g c2 t4 (THead (Flat Cast) t0 t3)
∀H9:eq T (THead (Bind Abbr) u1 t5) (THead (Flat Cast) t3 t2)
.∀H10:(eq T (THead (Bind Abbr) u2 w) t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
case pr0_zeta b:B H6:not (eq B b Abst) t5:T t6:T H7:pr0 t5 t6 u:T ⇒
the thesis becomes
∀H8:eq T (THead (Bind b) u (lift (S O) O t5)) (THead (Flat Cast) t3 t2)
.∀H9:(eq T t6 t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
suppose H8:
eq T (THead (Bind b) u (lift (S O) O t5)) (THead (Flat Cast) t3 t2)
suppose H9: eq T t6 t4
(H10)
we proceed by induction on H8 to prove
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind b) u (lift (S O) O t5) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) u (lift (S O) O t5) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
end of H10
consider H10
we proved
<λ:T.Prop>
CASE THead (Flat Cast) t3 t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
we proved
eq T t6 t4
→(not (eq B b Abst))→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
by (previous H9 H6 H7)
we proved ty3 g c2 t4 (THead (Flat Cast) t0 t3)
∀H8:eq T (THead (Bind b) u (lift (S O) O t5)) (THead (Flat Cast) t3 t2)
.∀H9:(eq T t6 t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
case pr0_tau t5:T t6:T H6:pr0 t5 t6 u:T ⇒
the thesis becomes
∀H7:eq T (THead (Flat Cast) u t5) (THead (Flat Cast) t3 t2)
.∀H8:(eq T t6 t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
suppose H7: eq T (THead (Flat Cast) u t5) (THead (Flat Cast) t3 t2)
suppose H8: eq T t6 t4
(H9)
by (f_equal . . . . . H7)
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u t5 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
<λ:T.T> CASE THead (Flat Cast) t3 t2 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
THead (Flat Cast) u t5
λe:T.<λ:T.T> CASE e OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
THead (Flat Cast) t3 t2
end of H9
(h1)
(H10)
by (f_equal . . . . . H7)
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u t5 OF TSort ⇒u | TLRef ⇒u | THead t7 ⇒t7
<λ:T.T> CASE THead (Flat Cast) t3 t2 OF TSort ⇒u | TLRef ⇒u | THead t7 ⇒t7
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u | TLRef ⇒u | THead t7 ⇒t7
THead (Flat Cast) u t5
λe:T.<λ:T.T> CASE e OF TSort ⇒u | TLRef ⇒u | THead t7 ⇒t7
THead (Flat Cast) t3 t2
end of H10
consider H10
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u t5 OF TSort ⇒u | TLRef ⇒u | THead t7 ⇒t7
<λ:T.T> CASE THead (Flat Cast) t3 t2 OF TSort ⇒u | TLRef ⇒u | THead t7 ⇒t7
that is equivalent to eq T u t3
by (sym_eq . . . previous)
we proved eq T t3 u
we proceed by induction on the previous result to prove (eq T t5 t2)→(eq T t6 t4)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
case refl_equal : ⇒
the thesis becomes (eq T t5 t2)→(eq T t6 t4)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
suppose H11: eq T t5 t2
by (sym_eq . . . H11)
we proved eq T t2 t5
we proceed by induction on the previous result to prove (eq T t6 t4)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
case refl_equal : ⇒
the thesis becomes (eq T t6 t4)→(pr0 t2 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
suppose H12: eq T t6 t4
by (sym_eq . . . H12)
we proved eq T t4 t6
we proceed by induction on the previous result to prove (pr0 t2 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
case refl_equal : ⇒
the thesis becomes (pr0 t2 t4)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
suppose H13: pr0 t2 t4
by (pr0_refl .)
we proved pr0 t3 t3
by (H3 . H4 . previous)
we proved ty3 g c2 t3 t0
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c2 t0 t
we proceed by induction on the previous result to prove ty3 g c2 t4 (THead (Flat Cast) t0 t3)
case ex_intro : x:T H14:ty3 g c2 t0 x ⇒
the thesis becomes ty3 g c2 t4 (THead (Flat Cast) t0 t3)
(h1)
by (pr0_refl .)
we proved pr0 t3 t3
by (H3 . H4 . previous)
we proved ty3 g c2 t3 t0
by (ty3_cast . . . . previous . H14)
ty3 g c2 (THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0)
end of h1
(h2) by (H1 . H4 . H13) we proved ty3 g c2 t4 t3
(h3)
by (pr0_refl .)
we proved pr0 t3 t3
by (pr0_tau . . previous .)
we proved pr0 (THead (Flat Cast) t0 t3) t3
by (pr2_free . . . previous)
we proved pr2 c2 (THead (Flat Cast) t0 t3) t3
by (pc3_pr2_x . . . previous)
pc3 c2 t3 (THead (Flat Cast) t0 t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c2 t4 (THead (Flat Cast) t0 t3)
we proved ty3 g c2 t4 (THead (Flat Cast) t0 t3)
(pr0 t2 t4)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
we proved (pr0 t2 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
(eq T t6 t4)→(pr0 t2 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
we proved (eq T t6 t4)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
(eq T t5 t2)→(eq T t6 t4)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
(eq T t5 t2)→(eq T t6 t4)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
end of h1
(h2)
consider H9
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u t5 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
<λ:T.T> CASE THead (Flat Cast) t3 t2 OF TSort ⇒t5 | TLRef ⇒t5 | THead t7⇒t7
eq T t5 t2
end of h2
by (h1 h2)
we proved (eq T t6 t4)→(pr0 t5 t6)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
by (previous H8 H6)
we proved ty3 g c2 t4 (THead (Flat Cast) t0 t3)
∀H7:eq T (THead (Flat Cast) u t5) (THead (Flat Cast) t3 t2)
.∀H8:(eq T t6 t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
eq T (THead (Flat Cast) t3 t2) (THead (Flat Cast) t3 t2)
→(eq T t4 t4)→(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
end of H6
(h1)
by (refl_equal . .)
eq T (THead (Flat Cast) t3 t2) (THead (Flat Cast) t3 t2)
end of h1
(h2)
by (refl_equal . .)
eq T t4 t4
end of h2
by (H6 h1 h2)
we proved ty3 g c2 t4 (THead (Flat Cast) t0 t3)
∀c2:C.∀H4:(wcpr0 c c2).∀t4:T.∀H5:(pr0 (THead (Flat Cast) t3 t2) t4).(ty3 g c2 t4 (THead (Flat Cast) t0 t3))
we proved ∀c2:C.(wcpr0 c1 c2)→∀t3:T.(pr0 t1 t3)→(ty3 g c2 t3 t)
we proved ∀g:G.∀c1:C.∀t1:T.∀t:T.(ty3 g c1 t1 t)→∀c2:C.(wcpr0 c1 c2)→∀t3:T.(pr0 t1 t3)→(ty3 g c2 t3 t)