DEFINITION ty3_fsubst0()
TYPE =
∀g:G
.∀c1:C
.∀t1:T
.∀t:T
.ty3 g c1 t1 t
→∀i:nat
.∀u:T.∀c2:C.∀t2:T.(fsubst0 i u c1 t1 c2 t2)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(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
∀i:nat
.∀u:T.∀c2:C.∀t3:T.(fsubst0 i u c1 t1 c2 t3)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(ty3 g c2 t3 t)
case ty3_conv : c:C t2:T t0:T H0:ty3 g c t2 t0 u:T t3:T :ty3 g c u t3 H4:pc3 c t3 t2 ⇒
the thesis becomes ∀i:nat.∀u0:T.∀c2:C.∀t4:T.∀H5:(fsubst0 i u0 c u c2 t4).∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t4 t2)
(H1) by induction hypothesis we know
∀i:nat
.∀u:T
.∀c2:C.∀t3:T.(fsubst0 i u c t2 c2 t3)→∀e:C.(getl i c (CHead e (Bind Abbr) u))→(ty3 g c2 t3 t0)
(H3) by induction hypothesis we know
∀i:nat
.∀u0:T.∀c2:C.∀t4:T.(fsubst0 i u0 c u c2 t4)→∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t4 t3)
assume i: nat
assume u0: T
assume c2: C
assume t4: T
suppose H5: fsubst0 i u0 c u c2 t4
we proceed by induction on H5 to prove ∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t4 t2)
case fsubst0_snd : t5:T H6:subst0 i u0 u t5 ⇒
the thesis becomes ∀e:C.∀H7:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c t5 t2)
assume e: C
suppose H7: getl i c (CHead e (Bind Abbr) u0)
by (fsubst0_snd . . . . . H6)
we proved fsubst0 i u0 c u c t5
by (H3 . . . . previous . H7)
we proved ty3 g c t5 t3
by (ty3_conv . . . . H0 . . previous H4)
we proved ty3 g c t5 t2
∀e:C.∀H7:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c t5 t2)
case fsubst0_fst : c3:C H6:csubst0 i u0 c c3 ⇒
the thesis becomes ∀e:C.∀H7:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 u t2)
assume e: C
suppose H7: getl i c (CHead e (Bind Abbr) u0)
(h1)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c t2 c3 t2
by (H1 . . . . previous . H7)
ty3 g c3 t2 t0
end of h1
(h2)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c u c3 u
by (H3 . . . . previous . H7)
ty3 g c3 u t3
end of h2
(h3)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c t3 c3 t3
by (pc3_fsubst0 . . . H4 . . . . previous . H7)
pc3 c3 t3 t2
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
we proved ty3 g c3 u t2
∀e:C.∀H7:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 u t2)
case fsubst0_both : t5:T H6:subst0 i u0 u t5 c3:C H7:csubst0 i u0 c c3 ⇒
the thesis becomes ∀e:C.∀H8:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 t5 t2)
assume e: C
suppose H8: getl i c (CHead e (Bind Abbr) u0)
(h1)
by (fsubst0_fst . . . . . H7)
we proved fsubst0 i u0 c t2 c3 t2
by (H1 . . . . previous . H8)
ty3 g c3 t2 t0
end of h1
(h2)
by (fsubst0_both . . . . . H6 . H7)
we proved fsubst0 i u0 c u c3 t5
by (H3 . . . . previous . H8)
ty3 g c3 t5 t3
end of h2
(h3)
by (fsubst0_fst . . . . . H7)
we proved fsubst0 i u0 c t3 c3 t3
by (pc3_fsubst0 . . . H4 . . . . previous . H8)
pc3 c3 t3 t2
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
we proved ty3 g c3 t5 t2
∀e:C.∀H8:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 t5 t2)
we proved ∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t4 t2)
∀i:nat.∀u0:T.∀c2:C.∀t4:T.∀H5:(fsubst0 i u0 c u c2 t4).∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t4 t2)
case ty3_sort : c:C m:nat ⇒
the thesis becomes
∀i:nat
.∀u:T
.∀c2:C
.∀t2:T
.∀H0:fsubst0 i u c (TSort m) c2 t2
.∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c2 t2 (TSort (next g m))
assume i: nat
assume u: T
assume c2: C
assume t2: T
suppose H0: fsubst0 i u c (TSort m) c2 t2
we proceed by induction on H0 to prove
∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c2 t2 (TSort (next g m))
case fsubst0_snd : t3:T H1:subst0 i u (TSort m) t3 ⇒
the thesis becomes
∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c t3 (TSort (next g m))
assume e: C
suppose : getl i c (CHead e (Bind Abbr) u)
by (subst0_gen_sort . . . . H1 .)
we proved ty3 g c t3 (TSort (next g m))
∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c t3 (TSort (next g m))
case fsubst0_fst : c3:C :csubst0 i u c c3 ⇒
the thesis becomes
∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c3 (TSort m) (TSort (next g m))
assume e: C
suppose : getl i c (CHead e (Bind Abbr) u)
by (ty3_sort . . .)
we proved ty3 g c3 (TSort m) (TSort (next g m))
∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c3 (TSort m) (TSort (next g m))
case fsubst0_both : t3:T H1:subst0 i u (TSort m) t3 c3:C :csubst0 i u c c3 ⇒
the thesis becomes
∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c3 t3 (TSort (next g m))
assume e: C
suppose : getl i c (CHead e (Bind Abbr) u)
by (subst0_gen_sort . . . . H1 .)
we proved ty3 g c3 t3 (TSort (next g m))
∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c3 t3 (TSort (next g m))
we proved
∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c2 t2 (TSort (next g m))
∀i:nat
.∀u:T
.∀c2:C
.∀t2:T
.∀H0:fsubst0 i u c (TSort m) c2 t2
.∀e:C
.getl i c (CHead e (Bind Abbr) u)
→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 H1:ty3 g d u t0 ⇒
the thesis becomes
∀i:nat
.∀u0:T
.∀c2:C
.∀t2:T
.∀H3:fsubst0 i u0 c (TLRef n) c2 t2
.∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t2 (lift (S n) O t0))
(H2) by induction hypothesis we know
∀i:nat
.∀u0:T.∀c2:C.∀t2:T.(fsubst0 i u0 d u c2 t2)→∀e:C.(getl i d (CHead e (Bind Abbr) u0))→(ty3 g c2 t2 t0)
assume i: nat
assume u0: T
assume c2: C
assume t2: T
suppose H3: fsubst0 i u0 c (TLRef n) c2 t2
we proceed by induction on H3 to prove ∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t2 (lift (S n) O t0))
case fsubst0_snd : t3:T H4:subst0 i u0 (TLRef n) t3 ⇒
the thesis becomes ∀e:C.∀H5:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c t3 (lift (S n) O t0))
assume e: C
suppose H5: getl i c (CHead e (Bind Abbr) u0)
by (subst0_gen_lref . . . . H4)
we proved land (eq nat n i) (eq T t3 (lift (S n) O u0))
we proceed by induction on the previous result to prove ty3 g c t3 (lift (S n) O t0)
case conj : H6:eq nat n i H7:eq T t3 (lift (S n) O u0) ⇒
the thesis becomes ty3 g c t3 (lift (S n) O t0)
(H8)
by (eq_ind_r . . . H5 . H6)
getl n c (CHead e (Bind Abbr) u0)
end of H8
(H9)
by (getl_mono . . . H0 . H8)
we proved eq C (CHead d (Bind Abbr) u) (CHead e (Bind Abbr) u0)
we proceed by induction on the previous result to prove getl n c (CHead e (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl n c (CHead e (Bind Abbr) u0)
end of H9
(H10)
by (getl_mono . . . H0 . H8)
we proved eq C (CHead d (Bind Abbr) u) (CHead e (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead e (Bind Abbr) u0 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead e (Bind Abbr) u0)
end of H10
(h1)
(H11)
by (getl_mono . . . H0 . H8)
we proved eq C (CHead d (Bind Abbr) u) (CHead e (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t4⇒t4
<λ:C.T> CASE CHead e (Bind Abbr) u0 OF CSort ⇒u | CHead t4⇒t4
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t4⇒t4 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t4⇒t4 (CHead e (Bind Abbr) u0)
end of H11
suppose H12: eq C d e
(H13)
by (eq_ind_r . . . H9 . H12)
getl n c (CHead d (Bind Abbr) u0)
end of H13
(H14)
consider H11
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t4⇒t4
<λ:C.T> CASE CHead e (Bind Abbr) u0 OF CSort ⇒u | CHead t4⇒t4
that is equivalent to eq T u u0
by (eq_ind_r . . . H13 . previous)
getl n c (CHead d (Bind Abbr) u)
end of H14
consider H11
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t4⇒t4
<λ:C.T> CASE CHead e (Bind Abbr) u0 OF CSort ⇒u | CHead t4⇒t4
that is equivalent to eq T u u0
we proceed by induction on the previous result to prove ty3 g c (lift (S n) O u0) (lift (S n) O t0)
case refl_equal : ⇒
the thesis becomes ty3 g c (lift (S n) O u) (lift (S n) O t0)
by (getl_drop . . . . . H14)
we proved drop (S n) O c d
by (ty3_lift . . . . H1 . . . previous)
ty3 g c (lift (S n) O u) (lift (S n) O t0)
we proved ty3 g c (lift (S n) O u0) (lift (S n) O t0)
(eq C d e)→(ty3 g c (lift (S n) O u0) (lift (S n) O t0))
end of h1
(h2)
consider H10
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead e (Bind Abbr) u0 OF CSort ⇒d | CHead c0 ⇒c0
eq C d e
end of h2
by (h1 h2)
we proved ty3 g c (lift (S n) O u0) (lift (S n) O t0)
by (eq_ind_r . . . previous . H7)
ty3 g c t3 (lift (S n) O t0)
we proved ty3 g c t3 (lift (S n) O t0)
∀e:C.∀H5:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c t3 (lift (S n) O t0))
case fsubst0_fst : c3:C H4:csubst0 i u0 c c3 ⇒
the thesis becomes
∀e:C
.∀H5:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 (TLRef n) (lift (S n) O t0))
assume e: C
suppose H5: getl i c (CHead e (Bind Abbr) u0)
(h1)
suppose H6: lt n i
(H7)
by (csubst0_getl_lt . . H6 . . . H4 . H0)
or4
getl n c3 (CHead d (Bind Abbr) u)
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c3 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) u0 u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c3 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) u0 e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c3 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) u0 u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) u0 e1 e2
end of H7
we proceed by induction on H7 to prove ty3 g c3 (TLRef n) (lift (S n) O t0)
case or4_intro0 : H8:getl n c3 (CHead d (Bind Abbr) u) ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O t0)
by (ty3_abbr . . . . . H8 . H1)
ty3 g c3 (TLRef n) (lift (S n) O t0)
case or4_intro1 : H8:ex3_4 B C T T λb:B.λe0:C.λu1:T.λ:T.eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b) u1) λb:B.λe0:C.λ:T.λw:T.getl n c3 (CHead e0 (Bind b) w) λ:B.λ:C.λu1:T.λw:T.subst0 (minus i (S n)) u0 u1 w ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O t0)
we proceed by induction on H8 to prove ty3 g c3 (TLRef n) (lift (S n) O t0)
case ex3_4_intro : x0:B x1:C x2:T x3:T H9:eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H10:getl n c3 (CHead x1 (Bind x0) x3) H11:subst0 (minus i (S n)) u0 x2 x3 ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O t0)
(H12)
by (f_equal . . . . . H9)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x2)
end of H12
(h1)
(H13)
by (f_equal . . . . . H9)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq
B
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead d (Bind Abbr) u
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead x1 (Bind x0) x2
end of H13
(h1)
(H14)
by (f_equal . . . . . H9)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t3⇒t3
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead x1 (Bind x0) x2)
end of H14
suppose H15: eq B Abbr x0
suppose H16: eq C d x1
(H17)
consider H14
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t3⇒t3
that is equivalent to eq T u x2
by (eq_ind_r . . . H11 . previous)
subst0 (minus i (S n)) u0 u x3
end of H17
(H18)
by (eq_ind_r . . . H10 . H16)
getl n c3 (CHead d (Bind x0) x3)
end of H18
(H19)
by (eq_ind_r . . . H18 . H15)
getl n c3 (CHead d (Bind Abbr) x3)
end of H19
(H20)
by (minus_x_Sy . . H6)
we proved eq nat (minus i n) (S (minus i (S n)))
we proceed by induction on the previous result to prove
getl
S (minus i (S n))
CHead d (Bind Abbr) x3
CHead e (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i n
CHead d (Bind Abbr) x3
CHead e (Bind Abbr) u0
(h1)
by (le_n .)
we proved le i i
by (csubst0_getl_ge . . previous . . . H4 . H5)
getl i c3 (CHead e (Bind Abbr) u0)
end of h1
(h2)
consider H6
we proved lt n i
that is equivalent to le (S n) i
by (le_S . . previous)
we proved le (S n) (S i)
by (le_S_n . . previous)
le n i
end of h2
by (getl_conf_le . . . h1 . . H19 h2)
getl
minus i n
CHead d (Bind Abbr) x3
CHead e (Bind Abbr) u0
getl
S (minus i (S n))
CHead d (Bind Abbr) x3
CHead e (Bind Abbr) u0
end of H20
(h1)
by (fsubst0_snd . . . . . H17)
fsubst0 (minus i (S n)) u0 d u d x3
end of h1
(h2)
by (getl_gen_S . . . . . H20)
we proved
getl
r (Bind Abbr) (minus i (S n))
d
CHead e (Bind Abbr) u0
getl (minus i (S n)) d (CHead e (Bind Abbr) u0)
end of h2
by (H2 . . . . h1 . h2)
we proved ty3 g d x3 t0
by (ty3_abbr . . . . . H19 . previous)
we proved ty3 g c3 (TLRef n) (lift (S n) O t0)
(eq B Abbr x0)→(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O t0))
end of h1
(h2)
consider H13
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq B Abbr x0
end of h2
by (h1 h2)
(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O t0))
end of h1
(h2)
consider H12
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
ty3 g c3 (TLRef n) (lift (S n) O t0)
ty3 g c3 (TLRef n) (lift (S n) O t0)
case or4_intro2 : H8:ex3_4 B C C T λb:B.λe1:C.λ:C.λu1:T.eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λu1:T.getl n c3 (CHead e2 (Bind b) u1) λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) u0 e1 e2 ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O t0)
we proceed by induction on H8 to prove ty3 g c3 (TLRef n) (lift (S n) O t0)
case ex3_4_intro : x0:B x1:C x2:C x3:T H9:eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10:getl n c3 (CHead x2 (Bind x0) x3) H11:csubst0 (minus i (S n)) u0 x1 x2 ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O t0)
(H12)
by (f_equal . . . . . H9)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x3)
end of H12
(h1)
(H13)
by (f_equal . . . . . H9)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq
B
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead d (Bind Abbr) u
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead x1 (Bind x0) x3
end of H13
(h1)
(H14)
by (f_equal . . . . . H9)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t3⇒t3
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead x1 (Bind x0) x3)
end of H14
suppose H15: eq B Abbr x0
suppose H16: eq C d x1
(H17)
consider H14
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t3⇒t3
that is equivalent to eq T u x3
by (eq_ind_r . . . H10 . previous)
getl n c3 (CHead x2 (Bind x0) u)
end of H17
(H18)
by (eq_ind_r . . . H11 . H16)
csubst0 (minus i (S n)) u0 d x2
end of H18
(H19)
by (eq_ind_r . . . H17 . H15)
getl n c3 (CHead x2 (Bind Abbr) u)
end of H19
(H20)
by (minus_x_Sy . . H6)
we proved eq nat (minus i n) (S (minus i (S n)))
we proceed by induction on the previous result to prove
getl
S (minus i (S n))
CHead x2 (Bind Abbr) u
CHead e (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i n
CHead x2 (Bind Abbr) u
CHead e (Bind Abbr) u0
(h1)
by (le_n .)
we proved le i i
by (csubst0_getl_ge . . previous . . . H4 . H5)
getl i c3 (CHead e (Bind Abbr) u0)
end of h1
(h2)
consider H6
we proved lt n i
that is equivalent to le (S n) i
by (le_S . . previous)
we proved le (S n) (S i)
by (le_S_n . . previous)
le n i
end of h2
by (getl_conf_le . . . h1 . . H19 h2)
getl
minus i n
CHead x2 (Bind Abbr) u
CHead e (Bind Abbr) u0
getl
S (minus i (S n))
CHead x2 (Bind Abbr) u
CHead e (Bind Abbr) u0
end of H20
(h1)
by (fsubst0_fst . . . . . H18)
fsubst0 (minus i (S n)) u0 d u x2 u
end of h1
(h2)
(h1)
by (le_n .)
le (minus i (S n)) (minus i (S n))
end of h1
(h2)
by (getl_gen_S . . . . . H20)
we proved
getl
r (Bind Abbr) (minus i (S n))
x2
CHead e (Bind Abbr) u0
getl (minus i (S n)) x2 (CHead e (Bind Abbr) u0)
end of h2
by (csubst0_getl_ge_back . . h1 . . . H18 . h2)
getl (minus i (S n)) d (CHead e (Bind Abbr) u0)
end of h2
by (H2 . . . . h1 . h2)
we proved ty3 g x2 u t0
by (ty3_abbr . . . . . H19 . previous)
we proved ty3 g c3 (TLRef n) (lift (S n) O t0)
(eq B Abbr x0)→(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O t0))
end of h1
(h2)
consider H13
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq B Abbr x0
end of h2
by (h1 h2)
(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O t0))
end of h1
(h2)
consider H12
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
ty3 g c3 (TLRef n) (lift (S n) O t0)
ty3 g c3 (TLRef n) (lift (S n) O t0)
case or4_intro3 : H8:ex4_5 B C C T T λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c3 (CHead e2 (Bind b) w) λ:B.λ:C.λ:C.λu1:T.λw:T.subst0 (minus i (S n)) u0 u1 w λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) u0 e1 e2 ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O t0)
we proceed by induction on H8 to prove ty3 g c3 (TLRef n) (lift (S n) O t0)
case ex4_5_intro : x0:B x1:C x2:C x3:T x4:T H9:eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10:getl n c3 (CHead x2 (Bind x0) x4) H11:subst0 (minus i (S n)) u0 x3 x4 H12:csubst0 (minus i (S n)) u0 x1 x2 ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O t0)
(H13)
by (f_equal . . . . . H9)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x3)
end of H13
(h1)
(H14)
by (f_equal . . . . . H9)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq
B
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead d (Bind Abbr) u
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead x1 (Bind x0) x3
end of H14
(h1)
(H15)
by (f_equal . . . . . H9)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t3⇒t3
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead x1 (Bind x0) x3)
end of H15
suppose H16: eq B Abbr x0
suppose H17: eq C d x1
(H18)
consider H15
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t3⇒t3
that is equivalent to eq T u x3
by (eq_ind_r . . . H11 . previous)
subst0 (minus i (S n)) u0 u x4
end of H18
(H19)
by (eq_ind_r . . . H12 . H17)
csubst0 (minus i (S n)) u0 d x2
end of H19
(H20)
by (eq_ind_r . . . H10 . H16)
getl n c3 (CHead x2 (Bind Abbr) x4)
end of H20
(H21)
by (minus_x_Sy . . H6)
we proved eq nat (minus i n) (S (minus i (S n)))
we proceed by induction on the previous result to prove
getl
S (minus i (S n))
CHead x2 (Bind Abbr) x4
CHead e (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i n
CHead x2 (Bind Abbr) x4
CHead e (Bind Abbr) u0
(h1)
by (le_n .)
we proved le i i
by (csubst0_getl_ge . . previous . . . H4 . H5)
getl i c3 (CHead e (Bind Abbr) u0)
end of h1
(h2)
consider H6
we proved lt n i
that is equivalent to le (S n) i
by (le_S . . previous)
we proved le (S n) (S i)
by (le_S_n . . previous)
le n i
end of h2
by (getl_conf_le . . . h1 . . H20 h2)
getl
minus i n
CHead x2 (Bind Abbr) x4
CHead e (Bind Abbr) u0
getl
S (minus i (S n))
CHead x2 (Bind Abbr) x4
CHead e (Bind Abbr) u0
end of H21
(h1)
by (fsubst0_both . . . . . H18 . H19)
fsubst0 (minus i (S n)) u0 d u x2 x4
end of h1
(h2)
(h1)
by (le_n .)
le (minus i (S n)) (minus i (S n))
end of h1
(h2)
by (getl_gen_S . . . . . H21)
we proved
getl
r (Bind Abbr) (minus i (S n))
x2
CHead e (Bind Abbr) u0
getl (minus i (S n)) x2 (CHead e (Bind Abbr) u0)
end of h2
by (csubst0_getl_ge_back . . h1 . . . H19 . h2)
getl (minus i (S n)) d (CHead e (Bind Abbr) u0)
end of h2
by (H2 . . . . h1 . h2)
we proved ty3 g x2 x4 t0
by (ty3_abbr . . . . . H20 . previous)
we proved ty3 g c3 (TLRef n) (lift (S n) O t0)
(eq B Abbr x0)→(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O t0))
end of h1
(h2)
consider H14
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq B Abbr x0
end of h2
by (h1 h2)
(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O t0))
end of h1
(h2)
consider H13
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
ty3 g c3 (TLRef n) (lift (S n) O t0)
ty3 g c3 (TLRef n) (lift (S n) O t0)
we proved ty3 g c3 (TLRef n) (lift (S n) O t0)
(lt n i)→(ty3 g c3 (TLRef n) (lift (S n) O t0))
end of h1
(h2)
suppose H6: le i n
by (csubst0_getl_ge . . H6 . . . H4 . H0)
we proved getl n c3 (CHead d (Bind Abbr) u)
by (ty3_abbr . . . . . previous . H1)
we proved ty3 g c3 (TLRef n) (lift (S n) O t0)
(le i n)→(ty3 g c3 (TLRef n) (lift (S n) O t0))
end of h2
by (lt_le_e . . . h1 h2)
we proved ty3 g c3 (TLRef n) (lift (S n) O t0)
∀e:C
.∀H5:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 (TLRef n) (lift (S n) O t0))
case fsubst0_both : t3:T H4:subst0 i u0 (TLRef n) t3 c3:C H5:csubst0 i u0 c c3 ⇒
the thesis becomes ∀e:C.∀H6:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 t3 (lift (S n) O t0))
assume e: C
suppose H6: getl i c (CHead e (Bind Abbr) u0)
by (subst0_gen_lref . . . . H4)
we proved land (eq nat n i) (eq T t3 (lift (S n) O u0))
we proceed by induction on the previous result to prove ty3 g c3 t3 (lift (S n) O t0)
case conj : H7:eq nat n i H8:eq T t3 (lift (S n) O u0) ⇒
the thesis becomes ty3 g c3 t3 (lift (S n) O t0)
(H9)
by (eq_ind_r . . . H6 . H7)
getl n c (CHead e (Bind Abbr) u0)
end of H9
(H10)
by (eq_ind_r . . . H5 . H7)
csubst0 n u0 c c3
end of H10
(H11)
by (getl_mono . . . H0 . H9)
we proved eq C (CHead d (Bind Abbr) u) (CHead e (Bind Abbr) u0)
we proceed by induction on the previous result to prove getl n c (CHead e (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl n c (CHead e (Bind Abbr) u0)
end of H11
(H12)
by (getl_mono . . . H0 . H9)
we proved eq C (CHead d (Bind Abbr) u) (CHead e (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead e (Bind Abbr) u0 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead e (Bind Abbr) u0)
end of H12
(h1)
(H13)
by (getl_mono . . . H0 . H9)
we proved eq C (CHead d (Bind Abbr) u) (CHead e (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t4⇒t4
<λ:C.T> CASE CHead e (Bind Abbr) u0 OF CSort ⇒u | CHead t4⇒t4
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t4⇒t4 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t4⇒t4 (CHead e (Bind Abbr) u0)
end of H13
suppose H14: eq C d e
(H15)
by (eq_ind_r . . . H11 . H14)
getl n c (CHead d (Bind Abbr) u0)
end of H15
(H16)
consider H13
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t4⇒t4
<λ:C.T> CASE CHead e (Bind Abbr) u0 OF CSort ⇒u | CHead t4⇒t4
that is equivalent to eq T u u0
by (eq_ind_r . . . H15 . previous)
getl n c (CHead d (Bind Abbr) u)
end of H16
(H17)
consider H13
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t4⇒t4
<λ:C.T> CASE CHead e (Bind Abbr) u0 OF CSort ⇒u | CHead t4⇒t4
that is equivalent to eq T u u0
by (eq_ind_r . . . H10 . previous)
csubst0 n u c c3
end of H17
consider H13
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t4⇒t4
<λ:C.T> CASE CHead e (Bind Abbr) u0 OF CSort ⇒u | CHead t4⇒t4
that is equivalent to eq T u u0
we proceed by induction on the previous result to prove ty3 g c3 (lift (S n) O u0) (lift (S n) O t0)
case refl_equal : ⇒
the thesis becomes ty3 g c3 (lift (S n) O u) (lift (S n) O t0)
by (le_n .)
we proved le n n
by (csubst0_getl_ge . . previous . . . H17 . H16)
we proved getl n c3 (CHead d (Bind Abbr) u)
by (getl_drop . . . . . previous)
we proved drop (S n) O c3 d
by (ty3_lift . . . . H1 . . . previous)
ty3 g c3 (lift (S n) O u) (lift (S n) O t0)
we proved ty3 g c3 (lift (S n) O u0) (lift (S n) O t0)
(eq C d e)→(ty3 g c3 (lift (S n) O u0) (lift (S n) O t0))
end of h1
(h2)
consider H12
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead e (Bind Abbr) u0 OF CSort ⇒d | CHead c0 ⇒c0
eq C d e
end of h2
by (h1 h2)
we proved ty3 g c3 (lift (S n) O u0) (lift (S n) O t0)
by (eq_ind_r . . . previous . H8)
ty3 g c3 t3 (lift (S n) O t0)
we proved ty3 g c3 t3 (lift (S n) O t0)
∀e:C.∀H6:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 t3 (lift (S n) O t0))
we proved ∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t2 (lift (S n) O t0))
∀i:nat
.∀u0:T
.∀c2:C
.∀t2:T
.∀H3:fsubst0 i u0 c (TLRef n) c2 t2
.∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(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 H1:ty3 g d u t0 ⇒
the thesis becomes
∀i:nat
.∀u0:T
.∀c2:C
.∀t2:T
.∀H3:fsubst0 i u0 c (TLRef n) c2 t2
.∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t2 (lift (S n) O u))
(H2) by induction hypothesis we know
∀i:nat
.∀u0:T.∀c2:C.∀t2:T.(fsubst0 i u0 d u c2 t2)→∀e:C.(getl i d (CHead e (Bind Abbr) u0))→(ty3 g c2 t2 t0)
assume i: nat
assume u0: T
assume c2: C
assume t2: T
suppose H3: fsubst0 i u0 c (TLRef n) c2 t2
we proceed by induction on H3 to prove ∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t2 (lift (S n) O u))
case fsubst0_snd : t3:T H4:subst0 i u0 (TLRef n) t3 ⇒
the thesis becomes ∀e:C.∀H5:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c t3 (lift (S n) O u))
assume e: C
suppose H5: getl i c (CHead e (Bind Abbr) u0)
by (subst0_gen_lref . . . . H4)
we proved land (eq nat n i) (eq T t3 (lift (S n) O u0))
we proceed by induction on the previous result to prove ty3 g c t3 (lift (S n) O u)
case conj : H6:eq nat n i H7:eq T t3 (lift (S n) O u0) ⇒
the thesis becomes ty3 g c t3 (lift (S n) O u)
(H8)
by (eq_ind_r . . . H5 . H6)
getl n c (CHead e (Bind Abbr) u0)
end of H8
(H10)
by (getl_mono . . . H0 . H8)
we proved eq C (CHead d (Bind Abst) u) (CHead e (Bind Abbr) u0)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead e (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead e (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H10
consider H10
we proved
<λ:C.Prop>
CASE CHead e (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove ty3 g c (lift (S n) O u0) (lift (S n) O u)
we proved ty3 g c (lift (S n) O u0) (lift (S n) O u)
by (eq_ind_r . . . previous . H7)
ty3 g c t3 (lift (S n) O u)
we proved ty3 g c t3 (lift (S n) O u)
∀e:C.∀H5:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c t3 (lift (S n) O u))
case fsubst0_fst : c3:C H4:csubst0 i u0 c c3 ⇒
the thesis becomes
∀e:C
.∀H5:getl i c (CHead e (Bind Abbr) u0)
.ty3 g c3 (TLRef n) (lift (S n) O u)
assume e: C
suppose H5: getl i c (CHead e (Bind Abbr) u0)
(h1)
suppose H6: lt n i
(H7)
by (csubst0_getl_lt . . H6 . . . H4 . H0)
or4
getl n c3 (CHead d (Bind Abst) u)
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead d (Bind Abst) u) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c3 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) u0 u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c3 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) u0 e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c3 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) u0 u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) u0 e1 e2
end of H7
we proceed by induction on H7 to prove ty3 g c3 (TLRef n) (lift (S n) O u)
case or4_intro0 : H8:getl n c3 (CHead d (Bind Abst) u) ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O u)
by (ty3_abst . . . . . H8 . H1)
ty3 g c3 (TLRef n) (lift (S n) O u)
case or4_intro1 : H8:ex3_4 B C T T λb:B.λe0:C.λu1:T.λ:T.eq C (CHead d (Bind Abst) u) (CHead e0 (Bind b) u1) λb:B.λe0:C.λ:T.λw:T.getl n c3 (CHead e0 (Bind b) w) λ:B.λ:C.λu1:T.λw:T.subst0 (minus i (S n)) u0 u1 w ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O u)
we proceed by induction on H8 to prove ty3 g c3 (TLRef n) (lift (S n) O u)
case ex3_4_intro : x0:B x1:C x2:T x3:T H9:eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x2) H10:getl n c3 (CHead x1 (Bind x0) x3) H11:subst0 (minus i (S n)) u0 x2 x3 ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O u)
(H12)
by (f_equal . . . . . H9)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abst) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x2)
end of H12
(h1)
(H13)
by (f_equal . . . . . H9)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq
B
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead d (Bind Abst) u
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead x1 (Bind x0) x2
end of H13
(h1)
(H14)
by (f_equal . . . . . H9)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t3⇒t3
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead d (Bind Abst) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead x1 (Bind x0) x2)
end of H14
suppose H15: eq B Abst x0
suppose H16: eq C d x1
(H17)
consider H14
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t3⇒t3
that is equivalent to eq T u x2
by (eq_ind_r . . . H11 . previous)
subst0 (minus i (S n)) u0 u x3
end of H17
(H18)
by (eq_ind_r . . . H10 . H16)
getl n c3 (CHead d (Bind x0) x3)
end of H18
(H19)
by (eq_ind_r . . . H18 . H15)
getl n c3 (CHead d (Bind Abst) x3)
end of H19
(H20)
by (minus_x_Sy . . H6)
we proved eq nat (minus i n) (S (minus i (S n)))
we proceed by induction on the previous result to prove
getl
S (minus i (S n))
CHead d (Bind Abst) x3
CHead e (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i n
CHead d (Bind Abst) x3
CHead e (Bind Abbr) u0
(h1)
by (le_n .)
we proved le i i
by (csubst0_getl_ge . . previous . . . H4 . H5)
getl i c3 (CHead e (Bind Abbr) u0)
end of h1
(h2)
consider H6
we proved lt n i
that is equivalent to le (S n) i
by (le_S . . previous)
we proved le (S n) (S i)
by (le_S_n . . previous)
le n i
end of h2
by (getl_conf_le . . . h1 . . H19 h2)
getl
minus i n
CHead d (Bind Abst) x3
CHead e (Bind Abbr) u0
getl
S (minus i (S n))
CHead d (Bind Abst) x3
CHead e (Bind Abbr) u0
end of H20
(h1)
by (getl_drop . . . . . H19)
we proved drop (S n) O c3 d
by (ty3_lift . . . . H1 . . . previous)
ty3 g c3 (lift (S n) O u) (lift (S n) O t0)
end of h1
(h2)
(h1)
by (fsubst0_snd . . . . . H17)
fsubst0 (minus i (S n)) u0 d u d x3
end of h1
(h2)
by (getl_gen_S . . . . . H20)
we proved
getl
r (Bind Abst) (minus i (S n))
d
CHead e (Bind Abbr) u0
getl (minus i (S n)) d (CHead e (Bind Abbr) u0)
end of h2
by (H2 . . . . h1 . h2)
we proved ty3 g d x3 t0
by (ty3_abst . . . . . H19 . previous)
ty3 g c3 (TLRef n) (lift (S n) O x3)
end of h2
(h3)
(h1)
by (getl_drop . . . . . H19)
drop (S n) O c3 d
end of h1
(h2)
(h1)
by (getl_gen_S . . . . . H20)
getl
r (Bind Abst) (minus i (S n))
d
CHead e (Bind Abbr) u0
end of h1
(h2) by (pr0_refl .) we proved pr0 u u
(h3)
consider H17
we proved subst0 (minus i (S n)) u0 u x3
subst0 (r (Bind Abst) (minus i (S n))) u0 u x3
end of h3
by (pr2_delta . . . . h1 . . h2 . h3)
we proved pr2 d u x3
by (pc3_pr2_x . . . previous)
pc3 d x3 u
end of h2
by (pc3_lift . . . . h1 . . h2)
pc3 c3 (lift (S n) O x3) (lift (S n) O u)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
we proved ty3 g c3 (TLRef n) (lift (S n) O u)
(eq B Abst x0)→(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O u))
end of h1
(h2)
consider H13
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq B Abst x0
end of h2
by (h1 h2)
(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O u))
end of h1
(h2)
consider H12
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
ty3 g c3 (TLRef n) (lift (S n) O u)
ty3 g c3 (TLRef n) (lift (S n) O u)
case or4_intro2 : H8:ex3_4 B C C T λb:B.λe1:C.λ:C.λu1:T.eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λu1:T.getl n c3 (CHead e2 (Bind b) u1) λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) u0 e1 e2 ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O u)
we proceed by induction on H8 to prove ty3 g c3 (TLRef n) (lift (S n) O u)
case ex3_4_intro : x0:B x1:C x2:C x3:T H9:eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x3) H10:getl n c3 (CHead x2 (Bind x0) x3) H11:csubst0 (minus i (S n)) u0 x1 x2 ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O u)
(H12)
by (f_equal . . . . . H9)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abst) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x3)
end of H12
(h1)
(H13)
by (f_equal . . . . . H9)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq
B
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead d (Bind Abst) u
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead x1 (Bind x0) x3
end of H13
(h1)
(H14)
by (f_equal . . . . . H9)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t3⇒t3
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead d (Bind Abst) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead x1 (Bind x0) x3)
end of H14
suppose H15: eq B Abst x0
suppose H16: eq C d x1
(H17)
consider H14
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t3⇒t3
that is equivalent to eq T u x3
by (eq_ind_r . . . H10 . previous)
getl n c3 (CHead x2 (Bind x0) u)
end of H17
(H18)
by (eq_ind_r . . . H11 . H16)
csubst0 (minus i (S n)) u0 d x2
end of H18
(H19)
by (eq_ind_r . . . H17 . H15)
getl n c3 (CHead x2 (Bind Abst) u)
end of H19
(H20)
by (minus_x_Sy . . H6)
we proved eq nat (minus i n) (S (minus i (S n)))
we proceed by induction on the previous result to prove
getl
S (minus i (S n))
CHead x2 (Bind Abst) u
CHead e (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i n
CHead x2 (Bind Abst) u
CHead e (Bind Abbr) u0
(h1)
by (le_n .)
we proved le i i
by (csubst0_getl_ge . . previous . . . H4 . H5)
getl i c3 (CHead e (Bind Abbr) u0)
end of h1
(h2)
consider H6
we proved lt n i
that is equivalent to le (S n) i
by (le_S . . previous)
we proved le (S n) (S i)
by (le_S_n . . previous)
le n i
end of h2
by (getl_conf_le . . . h1 . . H19 h2)
getl
minus i n
CHead x2 (Bind Abst) u
CHead e (Bind Abbr) u0
getl
S (minus i (S n))
CHead x2 (Bind Abst) u
CHead e (Bind Abbr) u0
end of H20
(h1)
by (fsubst0_fst . . . . . H18)
fsubst0 (minus i (S n)) u0 d u x2 u
end of h1
(h2)
(h1)
by (le_n .)
le (minus i (S n)) (minus i (S n))
end of h1
(h2)
by (getl_gen_S . . . . . H20)
we proved
getl
r (Bind Abst) (minus i (S n))
x2
CHead e (Bind Abbr) u0
getl (minus i (S n)) x2 (CHead e (Bind Abbr) u0)
end of h2
by (csubst0_getl_ge_back . . h1 . . . H18 . h2)
getl (minus i (S n)) d (CHead e (Bind Abbr) u0)
end of h2
by (H2 . . . . h1 . h2)
we proved ty3 g x2 u t0
by (ty3_abst . . . . . H19 . previous)
we proved ty3 g c3 (TLRef n) (lift (S n) O u)
(eq B Abst x0)→(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O u))
end of h1
(h2)
consider H13
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq B Abst x0
end of h2
by (h1 h2)
(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O u))
end of h1
(h2)
consider H12
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
ty3 g c3 (TLRef n) (lift (S n) O u)
ty3 g c3 (TLRef n) (lift (S n) O u)
case or4_intro3 : H8:ex4_5 B C C T T λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c3 (CHead e2 (Bind b) w) λ:B.λ:C.λ:C.λu1:T.λw:T.subst0 (minus i (S n)) u0 u1 w λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) u0 e1 e2 ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O u)
we proceed by induction on H8 to prove ty3 g c3 (TLRef n) (lift (S n) O u)
case ex4_5_intro : x0:B x1:C x2:C x3:T x4:T H9:eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x3) H10:getl n c3 (CHead x2 (Bind x0) x4) H11:subst0 (minus i (S n)) u0 x3 x4 H12:csubst0 (minus i (S n)) u0 x1 x2 ⇒
the thesis becomes ty3 g c3 (TLRef n) (lift (S n) O u)
(H13)
by (f_equal . . . . . H9)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abst) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x3)
end of H13
(h1)
(H14)
by (f_equal . . . . . H9)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq
B
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead d (Bind Abst) u
λe0:C
.<λ:C.B>
CASE e0 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead x1 (Bind x0) x3
end of H14
(h1)
(H15)
by (f_equal . . . . . H9)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t3⇒t3
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead d (Bind Abst) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t3⇒t3 (CHead x1 (Bind x0) x3)
end of H15
suppose H16: eq B Abst x0
suppose H17: eq C d x1
(H18)
consider H15
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t3⇒t3
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t3⇒t3
that is equivalent to eq T u x3
by (eq_ind_r . . . H11 . previous)
subst0 (minus i (S n)) u0 u x4
end of H18
(H19)
by (eq_ind_r . . . H12 . H17)
csubst0 (minus i (S n)) u0 d x2
end of H19
(H20)
by (eq_ind_r . . . H10 . H16)
getl n c3 (CHead x2 (Bind Abst) x4)
end of H20
(H21)
by (minus_x_Sy . . H6)
we proved eq nat (minus i n) (S (minus i (S n)))
we proceed by induction on the previous result to prove
getl
S (minus i (S n))
CHead x2 (Bind Abst) x4
CHead e (Bind Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus i n
CHead x2 (Bind Abst) x4
CHead e (Bind Abbr) u0
(h1)
by (le_n .)
we proved le i i
by (csubst0_getl_ge . . previous . . . H4 . H5)
getl i c3 (CHead e (Bind Abbr) u0)
end of h1
(h2)
consider H6
we proved lt n i
that is equivalent to le (S n) i
by (le_S . . previous)
we proved le (S n) (S i)
by (le_S_n . . previous)
le n i
end of h2
by (getl_conf_le . . . h1 . . H20 h2)
getl
minus i n
CHead x2 (Bind Abst) x4
CHead e (Bind Abbr) u0
getl
S (minus i (S n))
CHead x2 (Bind Abst) x4
CHead e (Bind Abbr) u0
end of H21
(h1)
(h1)
(h1)
by (fsubst0_fst . . . . . H19)
fsubst0 (minus i (S n)) u0 d u x2 u
end of h1
(h2)
(h1)
by (le_n .)
le (minus i (S n)) (minus i (S n))
end of h1
(h2)
by (getl_gen_S . . . . . H21)
we proved
getl
r (Bind Abst) (minus i (S n))
x2
CHead e (Bind Abbr) u0
getl (minus i (S n)) x2 (CHead e (Bind Abbr) u0)
end of h2
by (csubst0_getl_ge_back . . h1 . . . H19 . h2)
getl (minus i (S n)) d (CHead e (Bind Abbr) u0)
end of h2
by (H2 . . . . h1 . h2)
ty3 g x2 u t0
end of h1
(h2)
by (getl_drop . . . . . H20)
drop (S n) O c3 x2
end of h2
by (ty3_lift . . . . h1 . . . h2)
ty3 g c3 (lift (S n) O u) (lift (S n) O t0)
end of h1
(h2)
(h1)
by (fsubst0_both . . . . . H18 . H19)
fsubst0 (minus i (S n)) u0 d u x2 x4
end of h1
(h2)
(h1)
by (le_n .)
le (minus i (S n)) (minus i (S n))
end of h1
(h2)
by (getl_gen_S . . . . . H21)
we proved
getl
r (Bind Abst) (minus i (S n))
x2
CHead e (Bind Abbr) u0
getl (minus i (S n)) x2 (CHead e (Bind Abbr) u0)
end of h2
by (csubst0_getl_ge_back . . h1 . . . H19 . h2)
getl (minus i (S n)) d (CHead e (Bind Abbr) u0)
end of h2
by (H2 . . . . h1 . h2)
we proved ty3 g x2 x4 t0
by (ty3_abst . . . . . H20 . previous)
ty3 g c3 (TLRef n) (lift (S n) O x4)
end of h2
(h3)
(h1)
by (getl_drop . . . . . H20)
drop (S n) O c3 x2
end of h1
(h2)
(h1)
by (pc3_refl . .)
pc3 d u u
end of h1
(h2)
by (fsubst0_both . . . . . H18 . H19)
fsubst0 (minus i (S n)) u0 d u x2 x4
end of h2
(h3)
(h1)
by (le_n .)
le (minus i (S n)) (minus i (S n))
end of h1
(h2)
by (getl_gen_S . . . . . H21)
we proved
getl
r (Bind Abst) (minus i (S n))
x2
CHead e (Bind Abbr) u0
getl (minus i (S n)) x2 (CHead e (Bind Abbr) u0)
end of h2
by (csubst0_getl_ge_back . . h1 . . . H19 . h2)
getl (minus i (S n)) d (CHead e (Bind Abbr) u0)
end of h3
by (pc3_fsubst0 . . . h1 . . . . h2 . h3)
pc3 x2 x4 u
end of h2
by (pc3_lift . . . . h1 . . h2)
pc3 c3 (lift (S n) O x4) (lift (S n) O u)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
we proved ty3 g c3 (TLRef n) (lift (S n) O u)
(eq B Abst x0)→(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O u))
end of h1
(h2)
consider H14
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x3 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq B Abst x0
end of h2
by (h1 h2)
(eq C d x1)→(ty3 g c3 (TLRef n) (lift (S n) O u))
end of h1
(h2)
consider H13
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
ty3 g c3 (TLRef n) (lift (S n) O u)
ty3 g c3 (TLRef n) (lift (S n) O u)
we proved ty3 g c3 (TLRef n) (lift (S n) O u)
(lt n i)→(ty3 g c3 (TLRef n) (lift (S n) O u))
end of h1
(h2)
suppose H6: le i n
by (csubst0_getl_ge . . H6 . . . H4 . H0)
we proved getl n c3 (CHead d (Bind Abst) u)
by (ty3_abst . . . . . previous . H1)
we proved ty3 g c3 (TLRef n) (lift (S n) O u)
(le i n)→(ty3 g c3 (TLRef n) (lift (S n) O u))
end of h2
by (lt_le_e . . . h1 h2)
we proved ty3 g c3 (TLRef n) (lift (S n) O u)
∀e:C
.∀H5:getl i c (CHead e (Bind Abbr) u0)
.ty3 g c3 (TLRef n) (lift (S n) O u)
case fsubst0_both : t3:T H4:subst0 i u0 (TLRef n) t3 c3:C H5:csubst0 i u0 c c3 ⇒
the thesis becomes ∀e:C.∀H6:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 t3 (lift (S n) O u))
assume e: C
suppose H6: getl i c (CHead e (Bind Abbr) u0)
by (subst0_gen_lref . . . . H4)
we proved land (eq nat n i) (eq T t3 (lift (S n) O u0))
we proceed by induction on the previous result to prove ty3 g c3 t3 (lift (S n) O u)
case conj : H7:eq nat n i H8:eq T t3 (lift (S n) O u0) ⇒
the thesis becomes ty3 g c3 t3 (lift (S n) O u)
(H9)
by (eq_ind_r . . . H6 . H7)
getl n c (CHead e (Bind Abbr) u0)
end of H9
(H12)
by (getl_mono . . . H0 . H9)
we proved eq C (CHead d (Bind Abst) u) (CHead e (Bind Abbr) u0)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead e (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead e (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H12
consider H12
we proved
<λ:C.Prop>
CASE CHead e (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove ty3 g c3 (lift (S n) O u0) (lift (S n) O u)
we proved ty3 g c3 (lift (S n) O u0) (lift (S n) O u)
by (eq_ind_r . . . previous . H8)
ty3 g c3 t3 (lift (S n) O u)
we proved ty3 g c3 t3 (lift (S n) O u)
∀e:C.∀H6:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 t3 (lift (S n) O u))
we proved ∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t2 (lift (S n) O u))
∀i:nat
.∀u0:T
.∀c2:C
.∀t2:T
.∀H3:fsubst0 i u0 c (TLRef n) c2 t2
.∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t2 (lift (S n) O u))
case ty3_bind : c:C u:T t0:T H0:ty3 g c u t0 b:B t2:T t3:T H2:ty3 g (CHead c (Bind b) u) t2 t3 ⇒
the thesis becomes
∀i:nat
.∀u0:T
.∀c2:C
.∀t4:T
.∀H4:fsubst0 i u0 c (THead (Bind b) u t2) c2 t4
.∀e:C
.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t4 (THead (Bind b) u t3))
(H1) by induction hypothesis we know
∀i:nat
.∀u0:T.∀c2:C.∀t2:T.(fsubst0 i u0 c u c2 t2)→∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t2 t0)
(H3) by induction hypothesis we know
∀i:nat
.∀u0:T
.∀c2:C
.∀t4:T
.fsubst0 i u0 (CHead c (Bind b) u) t2 c2 t4
→∀e:C
.(getl i (CHead c (Bind b) u) (CHead e (Bind Abbr) u0))→(ty3 g c2 t4 t3)
assume i: nat
assume u0: T
assume c2: C
assume t4: T
suppose H4: fsubst0 i u0 c (THead (Bind b) u t2) c2 t4
we proceed by induction on H4 to prove
∀e:C
.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t4 (THead (Bind b) u t3))
case fsubst0_snd : t5:T H5:subst0 i u0 (THead (Bind b) u t2) t5 ⇒
the thesis becomes ∀e:C.∀H6:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c t5 (THead (Bind b) u t3))
assume e: C
suppose H6: getl i c (CHead e (Bind Abbr) u0)
by (subst0_gen_head . . . . . . H5)
we proved
or3
ex2 T λu2:T.eq T t5 (THead (Bind b) u2 t2) λu2:T.subst0 i u0 u u2
ex2 T λt2:T.eq T t5 (THead (Bind b) u t2) λt2:T.subst0 (s (Bind b) i) u0 t2 t2
ex3_2 T T λu2:T.λt2:T.eq T t5 (THead (Bind b) u2 t2) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt2:T.subst0 (s (Bind b) i) u0 t2 t2
we proceed by induction on the previous result to prove ty3 g c t5 (THead (Bind b) u t3)
case or3_intro0 : H7:ex2 T λu2:T.eq T t5 (THead (Bind b) u2 t2) λu2:T.subst0 i u0 u u2 ⇒
the thesis becomes ty3 g c t5 (THead (Bind b) u t3)
we proceed by induction on H7 to prove ty3 g c t5 (THead (Bind b) u t3)
case ex_intro2 : x:T H8:eq T t5 (THead (Bind b) x t2) H9:subst0 i u0 u x ⇒
the thesis becomes ty3 g c t5 (THead (Bind b) u t3)
by (ty3_correct . . . . H2)
we proved ex T λt:T.ty3 g (CHead c (Bind b) u) t3 t
we proceed by induction on the previous result to prove ty3 g c (THead (Bind b) x t2) (THead (Bind b) u t3)
case ex_intro : x0:T H10:ty3 g (CHead c (Bind b) u) t3 x0 ⇒
the thesis becomes ty3 g c (THead (Bind b) x t2) (THead (Bind b) u t3)
(h1)
by (csubst0_snd_bind . . . . . H9 .)
we proved csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c (Bind b) x)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c (Bind b) x) t2
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
we proved ty3 g (CHead c (Bind b) x) t2 t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c (Bind b) x) t3 t
we proceed by induction on the previous result to prove ty3 g c (THead (Bind b) x t2) (THead (Bind b) u t3)
case ex_intro : x1:T :ty3 g (CHead c (Bind b) x) t3 x1 ⇒
the thesis becomes ty3 g c (THead (Bind b) x t2) (THead (Bind b) u t3)
(h1)
by (ty3_bind . . . . H0 . . . H10)
ty3 g c (THead (Bind b) u t3) (THead (Bind b) u x0)
end of h1
(h2)
(h1)
by (fsubst0_snd . . . . . H9)
we proved fsubst0 i u0 c u c x
by (H1 . . . . previous . H6)
ty3 g c x t0
end of h1
(h2)
(h1)
by (csubst0_snd_bind . . . . . H9 .)
we proved csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c (Bind b) x)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c (Bind b) x) t2
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
ty3 g (CHead c (Bind b) x) t2 t3
end of h2
by (ty3_bind . . . . h1 . . . h2)
ty3 g c (THead (Bind b) x t2) (THead (Bind b) x t3)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3 c (THead (Bind b) u t3) (THead (Bind b) u t3)
end of h1
(h2)
by (subst0_fst . . . . H9 . .)
we proved subst0 i u0 (THead (Bind b) u t3) (THead (Bind b) x t3)
by (fsubst0_snd . . . . . previous)
fsubst0 i u0 c (THead (Bind b) u t3) c (THead (Bind b) x t3)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H6)
pc3 c (THead (Bind b) x t3) (THead (Bind b) u t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c (THead (Bind b) x t2) (THead (Bind b) u t3)
ty3 g c (THead (Bind b) x t2) (THead (Bind b) u t3)
we proved ty3 g c (THead (Bind b) x t2) (THead (Bind b) u t3)
by (eq_ind_r . . . previous . H8)
ty3 g c t5 (THead (Bind b) u t3)
ty3 g c t5 (THead (Bind b) u t3)
case or3_intro1 : H7:ex2 T λt6:T.eq T t5 (THead (Bind b) u t6) λt6:T.subst0 (s (Bind b) i) u0 t2 t6 ⇒
the thesis becomes ty3 g c t5 (THead (Bind b) u t3)
we proceed by induction on H7 to prove ty3 g c t5 (THead (Bind b) u t3)
case ex_intro2 : x:T H8:eq T t5 (THead (Bind b) u x) H9:subst0 (s (Bind b) i) u0 t2 x ⇒
the thesis becomes ty3 g c t5 (THead (Bind b) u t3)
(h1)
consider H9
we proved subst0 (s (Bind b) i) u0 t2 x
that is equivalent to subst0 (S i) u0 t2 x
by (fsubst0_snd . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c (Bind b) u) x
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
we proved ty3 g (CHead c (Bind b) u) x t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c (Bind b) u) t3 t
we proceed by induction on the previous result to prove ty3 g c (THead (Bind b) u x) (THead (Bind b) u t3)
case ex_intro : x0:T :ty3 g (CHead c (Bind b) u) t3 x0 ⇒
the thesis becomes ty3 g c (THead (Bind b) u x) (THead (Bind b) u t3)
(h1)
consider H9
we proved subst0 (s (Bind b) i) u0 t2 x
that is equivalent to subst0 (S i) u0 t2 x
by (fsubst0_snd . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c (Bind b) u) x
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
we proved ty3 g (CHead c (Bind b) u) x t3
by (ty3_bind . . . . H0 . . . previous)
ty3 g c (THead (Bind b) u x) (THead (Bind b) u t3)
we proved ty3 g c (THead (Bind b) u x) (THead (Bind b) u t3)
by (eq_ind_r . . . previous . H8)
ty3 g c t5 (THead (Bind b) u t3)
ty3 g c t5 (THead (Bind b) u t3)
case or3_intro2 : H7:ex3_2 T T λu2:T.λt6:T.eq T t5 (THead (Bind b) u2 t6) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt6:T.subst0 (s (Bind b) i) u0 t2 t6 ⇒
the thesis becomes ty3 g c t5 (THead (Bind b) u t3)
we proceed by induction on H7 to prove ty3 g c t5 (THead (Bind b) u t3)
case ex3_2_intro : x0:T x1:T H8:eq T t5 (THead (Bind b) x0 x1) H9:subst0 i u0 u x0 H10:subst0 (s (Bind b) i) u0 t2 x1 ⇒
the thesis becomes ty3 g c t5 (THead (Bind b) u t3)
by (ty3_correct . . . . H2)
we proved ex T λt:T.ty3 g (CHead c (Bind b) u) t3 t
we proceed by induction on the previous result to prove ty3 g c (THead (Bind b) x0 x1) (THead (Bind b) u t3)
case ex_intro : x:T H11:ty3 g (CHead c (Bind b) u) t3 x ⇒
the thesis becomes ty3 g c (THead (Bind b) x0 x1) (THead (Bind b) u t3)
(h1)
(h1)
consider H10
we proved subst0 (s (Bind b) i) u0 t2 x1
subst0 (S i) u0 t2 x1
end of h1
(h2)
by (csubst0_snd_bind . . . . . H9 .)
csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c (Bind b) x0)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c (Bind b) x0) x1
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
we proved ty3 g (CHead c (Bind b) x0) x1 t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c (Bind b) x0) t3 t
we proceed by induction on the previous result to prove ty3 g c (THead (Bind b) x0 x1) (THead (Bind b) u t3)
case ex_intro : x2:T :ty3 g (CHead c (Bind b) x0) t3 x2 ⇒
the thesis becomes ty3 g c (THead (Bind b) x0 x1) (THead (Bind b) u t3)
(h1)
by (ty3_bind . . . . H0 . . . H11)
ty3 g c (THead (Bind b) u t3) (THead (Bind b) u x)
end of h1
(h2)
(h1)
by (fsubst0_snd . . . . . H9)
we proved fsubst0 i u0 c u c x0
by (H1 . . . . previous . H6)
ty3 g c x0 t0
end of h1
(h2)
(h1)
(h1)
consider H10
we proved subst0 (s (Bind b) i) u0 t2 x1
subst0 (S i) u0 t2 x1
end of h1
(h2)
by (csubst0_snd_bind . . . . . H9 .)
csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c (Bind b) x0)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c (Bind b) x0) x1
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
ty3 g (CHead c (Bind b) x0) x1 t3
end of h2
by (ty3_bind . . . . h1 . . . h2)
ty3 g c (THead (Bind b) x0 x1) (THead (Bind b) x0 t3)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3 c (THead (Bind b) u t3) (THead (Bind b) u t3)
end of h1
(h2)
by (subst0_fst . . . . H9 . .)
we proved subst0 i u0 (THead (Bind b) u t3) (THead (Bind b) x0 t3)
by (fsubst0_snd . . . . . previous)
fsubst0 i u0 c (THead (Bind b) u t3) c (THead (Bind b) x0 t3)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H6)
pc3 c (THead (Bind b) x0 t3) (THead (Bind b) u t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c (THead (Bind b) x0 x1) (THead (Bind b) u t3)
ty3 g c (THead (Bind b) x0 x1) (THead (Bind b) u t3)
we proved ty3 g c (THead (Bind b) x0 x1) (THead (Bind b) u t3)
by (eq_ind_r . . . previous . H8)
ty3 g c t5 (THead (Bind b) u t3)
ty3 g c t5 (THead (Bind b) u t3)
we proved ty3 g c t5 (THead (Bind b) u t3)
∀e:C.∀H6:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c t5 (THead (Bind b) u t3))
case fsubst0_fst : c3:C H5:csubst0 i u0 c c3 ⇒
the thesis becomes
∀e:C
.∀H6:getl i c (CHead e (Bind Abbr) u0)
.ty3 g c3 (THead (Bind b) u t2) (THead (Bind b) u t3)
assume e: C
suppose H6: getl i c (CHead e (Bind Abbr) u0)
(h1)
by (csubst0_fst_bind . . . . . H5 .)
we proved csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c3 (Bind b) u)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) u) t2
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
we proved ty3 g (CHead c3 (Bind b) u) t2 t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c3 (Bind b) u) t3 t
we proceed by induction on the previous result to prove ty3 g c3 (THead (Bind b) u t2) (THead (Bind b) u t3)
case ex_intro : x:T :ty3 g (CHead c3 (Bind b) u) t3 x ⇒
the thesis becomes ty3 g c3 (THead (Bind b) u t2) (THead (Bind b) u t3)
(h1)
by (fsubst0_fst . . . . . H5)
we proved fsubst0 i u0 c u c3 u
by (H1 . . . . previous . H6)
ty3 g c3 u t0
end of h1
(h2)
(h1)
by (csubst0_fst_bind . . . . . H5 .)
we proved csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c3 (Bind b) u)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) u) t2
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
ty3 g (CHead c3 (Bind b) u) t2 t3
end of h2
by (ty3_bind . . . . h1 . . . h2)
ty3 g c3 (THead (Bind b) u t2) (THead (Bind b) u t3)
we proved ty3 g c3 (THead (Bind b) u t2) (THead (Bind b) u t3)
∀e:C
.∀H6:getl i c (CHead e (Bind Abbr) u0)
.ty3 g c3 (THead (Bind b) u t2) (THead (Bind b) u t3)
case fsubst0_both : t5:T H5:subst0 i u0 (THead (Bind b) u t2) t5 c3:C H6:csubst0 i u0 c c3 ⇒
the thesis becomes ∀e:C.∀H7:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 t5 (THead (Bind b) u t3))
assume e: C
suppose H7: getl i c (CHead e (Bind Abbr) u0)
by (subst0_gen_head . . . . . . H5)
we proved
or3
ex2 T λu2:T.eq T t5 (THead (Bind b) u2 t2) λu2:T.subst0 i u0 u u2
ex2 T λt2:T.eq T t5 (THead (Bind b) u t2) λt2:T.subst0 (s (Bind b) i) u0 t2 t2
ex3_2 T T λu2:T.λt2:T.eq T t5 (THead (Bind b) u2 t2) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt2:T.subst0 (s (Bind b) i) u0 t2 t2
we proceed by induction on the previous result to prove ty3 g c3 t5 (THead (Bind b) u t3)
case or3_intro0 : H8:ex2 T λu2:T.eq T t5 (THead (Bind b) u2 t2) λu2:T.subst0 i u0 u u2 ⇒
the thesis becomes ty3 g c3 t5 (THead (Bind b) u t3)
we proceed by induction on H8 to prove ty3 g c3 t5 (THead (Bind b) u t3)
case ex_intro2 : x:T H9:eq T t5 (THead (Bind b) x t2) H10:subst0 i u0 u x ⇒
the thesis becomes ty3 g c3 t5 (THead (Bind b) u t3)
(h1)
by (csubst0_fst_bind . . . . . H6 .)
we proved csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c3 (Bind b) u)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) u) t2
end of h1
(h2)
consider H7
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
we proved ty3 g (CHead c3 (Bind b) u) t2 t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c3 (Bind b) u) t3 t
we proceed by induction on the previous result to prove ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)
case ex_intro : x0:T H11:ty3 g (CHead c3 (Bind b) u) t3 x0 ⇒
the thesis becomes ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)
by (ty3_correct . . . . H11)
we proved ex T λt:T.ty3 g (CHead c3 (Bind b) u) x0 t
we proceed by induction on the previous result to prove ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)
case ex_intro : x1:T :ty3 g (CHead c3 (Bind b) u) x0 x1 ⇒
the thesis becomes ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)
(h1)
by (csubst0_both_bind . . . . . H10 . . H6)
we proved csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c3 (Bind b) x)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) x) t2
end of h1
(h2)
consider H7
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
we proved ty3 g (CHead c3 (Bind b) x) t2 t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c3 (Bind b) x) t3 t
we proceed by induction on the previous result to prove ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)
case ex_intro : x2:T :ty3 g (CHead c3 (Bind b) x) t3 x2 ⇒
the thesis becomes ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)
(h1)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c u c3 u
by (H1 . . . . previous . H7)
we proved ty3 g c3 u t0
by (ty3_bind . . . . previous . . . H11)
ty3 g c3 (THead (Bind b) u t3) (THead (Bind b) u x0)
end of h1
(h2)
(h1)
by (fsubst0_both . . . . . H10 . H6)
we proved fsubst0 i u0 c u c3 x
by (H1 . . . . previous . H7)
ty3 g c3 x t0
end of h1
(h2)
(h1)
by (csubst0_both_bind . . . . . H10 . . H6)
we proved csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c3 (Bind b) x)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) x) t2
end of h1
(h2)
consider H7
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
ty3 g (CHead c3 (Bind b) x) t2 t3
end of h2
by (ty3_bind . . . . h1 . . . h2)
ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) x t3)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3 c (THead (Bind b) u t3) (THead (Bind b) u t3)
end of h1
(h2)
by (subst0_fst . . . . H10 . .)
we proved subst0 i u0 (THead (Bind b) u t3) (THead (Bind b) x t3)
by (fsubst0_both . . . . . previous . H6)
fsubst0 i u0 c (THead (Bind b) u t3) c3 (THead (Bind b) x t3)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H7)
pc3 c3 (THead (Bind b) x t3) (THead (Bind b) u t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)
ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)
ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)
we proved ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)
by (eq_ind_r . . . previous . H9)
ty3 g c3 t5 (THead (Bind b) u t3)
ty3 g c3 t5 (THead (Bind b) u t3)
case or3_intro1 : H8:ex2 T λt6:T.eq T t5 (THead (Bind b) u t6) λt6:T.subst0 (s (Bind b) i) u0 t2 t6 ⇒
the thesis becomes ty3 g c3 t5 (THead (Bind b) u t3)
we proceed by induction on H8 to prove ty3 g c3 t5 (THead (Bind b) u t3)
case ex_intro2 : x:T H9:eq T t5 (THead (Bind b) u x) H10:subst0 (s (Bind b) i) u0 t2 x ⇒
the thesis becomes ty3 g c3 t5 (THead (Bind b) u t3)
(h1)
(h1)
consider H10
we proved subst0 (s (Bind b) i) u0 t2 x
subst0 (S i) u0 t2 x
end of h1
(h2)
by (csubst0_fst_bind . . . . . H6 .)
csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c3 (Bind b) u)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) u) x
end of h1
(h2)
consider H7
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
we proved ty3 g (CHead c3 (Bind b) u) x t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c3 (Bind b) u) t3 t
we proceed by induction on the previous result to prove ty3 g c3 (THead (Bind b) u x) (THead (Bind b) u t3)
case ex_intro : x0:T :ty3 g (CHead c3 (Bind b) u) t3 x0 ⇒
the thesis becomes ty3 g c3 (THead (Bind b) u x) (THead (Bind b) u t3)
(h1)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c u c3 u
by (H1 . . . . previous . H7)
ty3 g c3 u t0
end of h1
(h2)
(h1)
(h1)
consider H10
we proved subst0 (s (Bind b) i) u0 t2 x
subst0 (S i) u0 t2 x
end of h1
(h2)
by (csubst0_fst_bind . . . . . H6 .)
csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c3 (Bind b) u)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) u) x
end of h1
(h2)
consider H7
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
ty3 g (CHead c3 (Bind b) u) x t3
end of h2
by (ty3_bind . . . . h1 . . . h2)
ty3 g c3 (THead (Bind b) u x) (THead (Bind b) u t3)
we proved ty3 g c3 (THead (Bind b) u x) (THead (Bind b) u t3)
by (eq_ind_r . . . previous . H9)
ty3 g c3 t5 (THead (Bind b) u t3)
ty3 g c3 t5 (THead (Bind b) u t3)
case or3_intro2 : H8:ex3_2 T T λu2:T.λt6:T.eq T t5 (THead (Bind b) u2 t6) λu2:T.λ:T.subst0 i u0 u u2 λ:T.λt6:T.subst0 (s (Bind b) i) u0 t2 t6 ⇒
the thesis becomes ty3 g c3 t5 (THead (Bind b) u t3)
we proceed by induction on H8 to prove ty3 g c3 t5 (THead (Bind b) u t3)
case ex3_2_intro : x0:T x1:T H9:eq T t5 (THead (Bind b) x0 x1) H10:subst0 i u0 u x0 H11:subst0 (s (Bind b) i) u0 t2 x1 ⇒
the thesis becomes ty3 g c3 t5 (THead (Bind b) u t3)
(h1)
by (csubst0_fst_bind . . . . . H6 .)
we proved csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c3 (Bind b) u)
by (fsubst0_fst . . . . . previous)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) u) t2
end of h1
(h2)
consider H7
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
we proved ty3 g (CHead c3 (Bind b) u) t2 t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c3 (Bind b) u) t3 t
we proceed by induction on the previous result to prove ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)
case ex_intro : x:T H12:ty3 g (CHead c3 (Bind b) u) t3 x ⇒
the thesis becomes ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)
by (ty3_correct . . . . H12)
we proved ex T λt:T.ty3 g (CHead c3 (Bind b) u) x t
we proceed by induction on the previous result to prove ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)
case ex_intro : x2:T :ty3 g (CHead c3 (Bind b) u) x x2 ⇒
the thesis becomes ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)
(h1)
(h1)
consider H11
we proved subst0 (s (Bind b) i) u0 t2 x1
subst0 (S i) u0 t2 x1
end of h1
(h2)
by (csubst0_both_bind . . . . . H10 . . H6)
csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c3 (Bind b) x0)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) x0) x1
end of h1
(h2)
consider H7
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
we proved ty3 g (CHead c3 (Bind b) x0) x1 t3
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g (CHead c3 (Bind b) x0) t3 t
we proceed by induction on the previous result to prove ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)
case ex_intro : x3:T :ty3 g (CHead c3 (Bind b) x0) t3 x3 ⇒
the thesis becomes ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)
(h1)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c u c3 u
by (H1 . . . . previous . H7)
we proved ty3 g c3 u t0
by (ty3_bind . . . . previous . . . H12)
ty3 g c3 (THead (Bind b) u t3) (THead (Bind b) u x)
end of h1
(h2)
(h1)
by (fsubst0_both . . . . . H10 . H6)
we proved fsubst0 i u0 c u c3 x0
by (H1 . . . . previous . H7)
ty3 g c3 x0 t0
end of h1
(h2)
(h1)
(h1)
consider H11
we proved subst0 (s (Bind b) i) u0 t2 x1
subst0 (S i) u0 t2 x1
end of h1
(h2)
by (csubst0_both_bind . . . . . H10 . . H6)
csubst0 (S i) u0 (CHead c (Bind b) u) (CHead c3 (Bind b) x0)
end of h2
by (fsubst0_both . . . . . h1 . h2)
fsubst0 (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) x0) x1
end of h1
(h2)
consider H7
we proved getl i c (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) i) c (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S i) (CHead c (Bind b) u) (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
ty3 g (CHead c3 (Bind b) x0) x1 t3
end of h2
by (ty3_bind . . . . h1 . . . h2)
ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) x0 t3)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3 c (THead (Bind b) u t3) (THead (Bind b) u t3)
end of h1
(h2)
by (subst0_fst . . . . H10 . .)
we proved subst0 i u0 (THead (Bind b) u t3) (THead (Bind b) x0 t3)
by (fsubst0_both . . . . . previous . H6)
fsubst0 i u0 c (THead (Bind b) u t3) c3 (THead (Bind b) x0 t3)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H7)
pc3 c3 (THead (Bind b) x0 t3) (THead (Bind b) u t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)
ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)
ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)
we proved ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)
by (eq_ind_r . . . previous . H9)
ty3 g c3 t5 (THead (Bind b) u t3)
ty3 g c3 t5 (THead (Bind b) u t3)
we proved ty3 g c3 t5 (THead (Bind b) u t3)
∀e:C.∀H7:(getl i c (CHead e (Bind Abbr) u0)).(ty3 g c3 t5 (THead (Bind b) u t3))
we proved
∀e:C
.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t4 (THead (Bind b) u t3))
∀i:nat
.∀u0:T
.∀c2:C
.∀t4:T
.∀H4:fsubst0 i u0 c (THead (Bind b) u t2) c2 t4
.∀e:C
.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t4 (THead (Bind b) u t3))
case ty3_appl : c:C w:T u:T H0:ty3 g c w u v:T t0:T H2:ty3 g c v (THead (Bind Abst) u t0) ⇒
the thesis becomes
∀i:nat
.∀u0:T
.∀c2:C
.∀t2:T
.∀H4:fsubst0 i u0 c (THead (Flat Appl) w v) c2 t2
.∀e:C
.getl i c (CHead e (Bind Abbr) u0)
→ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
(H1) by induction hypothesis we know
∀i:nat
.∀u0:T.∀c2:C.∀t2:T.(fsubst0 i u0 c w c2 t2)→∀e:C.(getl i c (CHead e (Bind Abbr) u0))→(ty3 g c2 t2 u)
(H3) by induction hypothesis we know
∀i:nat
.∀u0:T
.∀c2:C
.∀t2:T
.fsubst0 i u0 c v c2 t2
→∀e:C
.getl i c (CHead e (Bind Abbr) u0)
→ty3 g c2 t2 (THead (Bind Abst) u t0)
assume i: nat
assume u0: T
assume c2: C
assume t2: T
suppose H4: fsubst0 i u0 c (THead (Flat Appl) w v) c2 t2
we proceed by induction on H4 to prove
∀e:C
.getl i c (CHead e (Bind Abbr) u0)
→ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case fsubst0_snd : t3:T H5:subst0 i u0 (THead (Flat Appl) w v) t3 ⇒
the thesis becomes
∀e:C
.∀H6:getl i c (CHead e (Bind Abbr) u0)
.ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
assume e: C
suppose H6: getl i c (CHead e (Bind Abbr) u0)
by (subst0_gen_head . . . . . . H5)
we proved
or3
ex2 T λu2:T.eq T t3 (THead (Flat Appl) u2 v) λu2:T.subst0 i u0 w u2
ex2 T λt2:T.eq T t3 (THead (Flat Appl) w t2) λt2:T.subst0 (s (Flat Appl) i) u0 v t2
ex3_2
T
T
λu2:T.λt2:T.eq T t3 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.subst0 i u0 w u2
λ:T.λt2:T.subst0 (s (Flat Appl) i) u0 v t2
we proceed by induction on the previous result to prove ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case or3_intro0 : H7:ex2 T λu2:T.eq T t3 (THead (Flat Appl) u2 v) λu2:T.subst0 i u0 w u2 ⇒
the thesis becomes ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
we proceed by induction on H7 to prove ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case ex_intro2 : x:T H8:eq T t3 (THead (Flat Appl) x v) H9:subst0 i u0 w x ⇒
the thesis becomes ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
by (ty3_correct . . . . H2)
we proved ex T λt:T.ty3 g c (THead (Bind Abst) u t0) t
we proceed by induction on the previous result to prove
ty3
g
c
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex_intro : x0:T H10:ty3 g c (THead (Bind Abst) u t0) x0 ⇒
the thesis becomes
ty3
g
c
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (ty3_gen_bind . . . . . . H10)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c (THead (Bind Abst) u t2) x0
λ:T.λt:T.ty3 g c u t
λt2:T.λ:T.ty3 g (CHead c (Bind Abst) u) t0 t2
we proceed by induction on the previous result to prove
ty3
g
c
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex3_2_intro : x1:T x2:T :pc3 c (THead (Bind Abst) u x1) x0 :ty3 g c u x2 H13:ty3 g (CHead c (Bind Abst) u) t0 x1 ⇒
the thesis becomes
ty3
g
c
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (fsubst0_snd . . . . . H9)
we proved fsubst0 i u0 c w c x
by (H1 . . . . previous . H6)
we proved ty3 g c x u
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c u t
we proceed by induction on the previous result to prove
ty3
g
c
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex_intro : x3:T H14:ty3 g c u x3 ⇒
the thesis becomes
ty3
g
c
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
(h1)
by (ty3_bind . . . . H14 . . . H13)
we proved ty3 g c (THead (Bind Abst) u t0) (THead (Bind Abst) u x1)
by (ty3_appl . . . . H0 . . previous)
ty3
g
c
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u x1)
end of h1
(h2)
by (fsubst0_snd . . . . . H9)
we proved fsubst0 i u0 c w c x
by (H1 . . . . previous . H6)
we proved ty3 g c x u
by (ty3_appl . . . . previous . . H2)
ty3
g
c
THead (Flat Appl) x v
THead (Flat Appl) x (THead (Bind Abst) u t0)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3
c
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u t0)
end of h1
(h2)
by (subst0_fst . . . . H9 . .)
we proved
subst0
i
u0
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) x (THead (Bind Abst) u t0)
by (fsubst0_snd . . . . . previous)
fsubst0
i
u0
c
THead (Flat Appl) w (THead (Bind Abst) u t0)
c
THead (Flat Appl) x (THead (Bind Abst) u t0)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H6)
pc3
c
THead (Flat Appl) x (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
c
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
we proved
ty3
g
c
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (eq_ind_r . . . previous . H8)
ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case or3_intro1 : H7:ex2 T λt4:T.eq T t3 (THead (Flat Appl) w t4) λt4:T.subst0 (s (Flat Appl) i) u0 v t4 ⇒
the thesis becomes ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
we proceed by induction on H7 to prove ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case ex_intro2 : x:T H8:eq T t3 (THead (Flat Appl) w x) H9:subst0 (s (Flat Appl) i) u0 v x ⇒
the thesis becomes ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
(h1)
by (fsubst0_snd . . . . . H9)
fsubst0 (s (Flat Appl) i) u0 c v c x
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u0)
getl (s (Flat Appl) i) c (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
we proved ty3 g c x (THead (Bind Abst) u t0)
by (ty3_appl . . . . H0 . . previous)
we proved
ty3
g
c
THead (Flat Appl) w x
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (eq_ind_r . . . previous . H8)
ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case or3_intro2 : H7:ex3_2 T T λu2:T.λt4:T.eq T t3 (THead (Flat Appl) u2 t4) λu2:T.λ:T.subst0 i u0 w u2 λ:T.λt4:T.subst0 (s (Flat Appl) i) u0 v t4 ⇒
the thesis becomes ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
we proceed by induction on H7 to prove ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case ex3_2_intro : x0:T x1:T H8:eq T t3 (THead (Flat Appl) x0 x1) H9:subst0 i u0 w x0 H10:subst0 (s (Flat Appl) i) u0 v x1 ⇒
the thesis becomes ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
by (ty3_correct . . . . H2)
we proved ex T λt:T.ty3 g c (THead (Bind Abst) u t0) t
we proceed by induction on the previous result to prove
ty3
g
c
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex_intro : x:T H11:ty3 g c (THead (Bind Abst) u t0) x ⇒
the thesis becomes
ty3
g
c
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (ty3_gen_bind . . . . . . H11)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c (THead (Bind Abst) u t2) x
λ:T.λt:T.ty3 g c u t
λt2:T.λ:T.ty3 g (CHead c (Bind Abst) u) t0 t2
we proceed by induction on the previous result to prove
ty3
g
c
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex3_2_intro : x2:T x3:T :pc3 c (THead (Bind Abst) u x2) x :ty3 g c u x3 H14:ty3 g (CHead c (Bind Abst) u) t0 x2 ⇒
the thesis becomes
ty3
g
c
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (ty3_correct . . . . H0)
we proved ex T λt:T.ty3 g c u t
we proceed by induction on the previous result to prove
ty3
g
c
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex_intro : x4:T H15:ty3 g c u x4 ⇒
the thesis becomes
ty3
g
c
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
(h1)
by (ty3_bind . . . . H15 . . . H14)
we proved ty3 g c (THead (Bind Abst) u t0) (THead (Bind Abst) u x2)
by (ty3_appl . . . . H0 . . previous)
ty3
g
c
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u x2)
end of h1
(h2)
(h1)
by (fsubst0_snd . . . . . H9)
we proved fsubst0 i u0 c w c x0
by (H1 . . . . previous . H6)
ty3 g c x0 u
end of h1
(h2)
(h1)
by (fsubst0_snd . . . . . H10)
fsubst0 (s (Flat Appl) i) u0 c v c x1
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u0)
getl (s (Flat Appl) i) c (CHead e (Bind Abbr) u0)
end of h2
by (H3 . . . . h1 . h2)
ty3 g c x1 (THead (Bind Abst) u t0)
end of h2
by (ty3_appl . . . . h1 . . h2)
ty3
g
c
THead (Flat Appl) x0 x1
THead (Flat Appl) x0 (THead (Bind Abst) u t0)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3
c
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u t0)
end of h1
(h2)
by (subst0_fst . . . . H9 . .)
we proved
subst0
i
u0
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) x0 (THead (Bind Abst) u t0)
by (fsubst0_snd . . . . . previous)
fsubst0
i
u0
c
THead (Flat Appl) w (THead (Bind Abst) u t0)
c
THead (Flat Appl) x0 (THead (Bind Abst) u t0)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H6)
pc3
c
THead (Flat Appl) x0 (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
c
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
we proved
ty3
g
c
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (eq_ind_r . . . previous . H8)
ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
we proved ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
∀e:C
.∀H6:getl i c (CHead e (Bind Abbr) u0)
.ty3 g c t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case fsubst0_fst : c3:C H5:csubst0 i u0 c c3 ⇒
the thesis becomes
∀e:C
.∀H6:getl i c (CHead e (Bind Abbr) u0)
.ty3
g
c3
THead (Flat Appl) w v
THead (Flat Appl) w (THead (Bind Abst) u t0)
assume e: C
suppose H6: getl i c (CHead e (Bind Abbr) u0)
(h1)
by (fsubst0_fst . . . . . H5)
we proved fsubst0 i u0 c w c3 w
by (H1 . . . . previous . H6)
ty3 g c3 w u
end of h1
(h2)
by (fsubst0_fst . . . . . H5)
we proved fsubst0 i u0 c v c3 v
by (H3 . . . . previous . H6)
ty3 g c3 v (THead (Bind Abst) u t0)
end of h2
by (ty3_appl . . . . h1 . . h2)
we proved
ty3
g
c3
THead (Flat Appl) w v
THead (Flat Appl) w (THead (Bind Abst) u t0)
∀e:C
.∀H6:getl i c (CHead e (Bind Abbr) u0)
.ty3
g
c3
THead (Flat Appl) w v
THead (Flat Appl) w (THead (Bind Abst) u t0)
case fsubst0_both : t3:T H5:subst0 i u0 (THead (Flat Appl) w v) t3 c3:C H6:csubst0 i u0 c c3 ⇒
the thesis becomes
∀e:C
.∀H7:getl i c (CHead e (Bind Abbr) u0)
.ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
assume e: C
suppose H7: getl i c (CHead e (Bind Abbr) u0)
by (subst0_gen_head . . . . . . H5)
we proved
or3
ex2 T λu2:T.eq T t3 (THead (Flat Appl) u2 v) λu2:T.subst0 i u0 w u2
ex2 T λt2:T.eq T t3 (THead (Flat Appl) w t2) λt2:T.subst0 (s (Flat Appl) i) u0 v t2
ex3_2
T
T
λu2:T.λt2:T.eq T t3 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.subst0 i u0 w u2
λ:T.λt2:T.subst0 (s (Flat Appl) i) u0 v t2
we proceed by induction on the previous result to prove ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case or3_intro0 : H8:ex2 T λu2:T.eq T t3 (THead (Flat Appl) u2 v) λu2:T.subst0 i u0 w u2 ⇒
the thesis becomes ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
we proceed by induction on H8 to prove ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case ex_intro2 : x:T H9:eq T t3 (THead (Flat Appl) x v) H10:subst0 i u0 w x ⇒
the thesis becomes ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c v c3 v
by (H3 . . . . previous . H7)
we proved ty3 g c3 v (THead (Bind Abst) u t0)
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c3 (THead (Bind Abst) u t0) t
we proceed by induction on the previous result to prove
ty3
g
c3
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex_intro : x0:T H11:ty3 g c3 (THead (Bind Abst) u t0) x0 ⇒
the thesis becomes
ty3
g
c3
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (ty3_gen_bind . . . . . . H11)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c3 (THead (Bind Abst) u t2) x0
λ:T.λt:T.ty3 g c3 u t
λt2:T.λ:T.ty3 g (CHead c3 (Bind Abst) u) t0 t2
we proceed by induction on the previous result to prove
ty3
g
c3
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex3_2_intro : x1:T x2:T :pc3 c3 (THead (Bind Abst) u x1) x0 H13:ty3 g c3 u x2 H14:ty3 g (CHead c3 (Bind Abst) u) t0 x1 ⇒
the thesis becomes
ty3
g
c3
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
(h1)
(h1)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c w c3 w
by (H1 . . . . previous . H7)
ty3 g c3 w u
end of h1
(h2)
by (ty3_bind . . . . H13 . . . H14)
ty3 g c3 (THead (Bind Abst) u t0) (THead (Bind Abst) u x1)
end of h2
by (ty3_appl . . . . h1 . . h2)
ty3
g
c3
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u x1)
end of h1
(h2)
(h1)
by (fsubst0_both . . . . . H10 . H6)
we proved fsubst0 i u0 c w c3 x
by (H1 . . . . previous . H7)
ty3 g c3 x u
end of h1
(h2)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c v c3 v
by (H3 . . . . previous . H7)
ty3 g c3 v (THead (Bind Abst) u t0)
end of h2
by (ty3_appl . . . . h1 . . h2)
ty3
g
c3
THead (Flat Appl) x v
THead (Flat Appl) x (THead (Bind Abst) u t0)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3
c
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u t0)
end of h1
(h2)
by (subst0_fst . . . . H10 . .)
we proved
subst0
i
u0
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) x (THead (Bind Abst) u t0)
by (fsubst0_both . . . . . previous . H6)
fsubst0
i
u0
c
THead (Flat Appl) w (THead (Bind Abst) u t0)
c3
THead (Flat Appl) x (THead (Bind Abst) u t0)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H7)
pc3
c3
THead (Flat Appl) x (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
c3
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c3
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
we proved
ty3
g
c3
THead (Flat Appl) x v
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (eq_ind_r . . . previous . H9)
ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case or3_intro1 : H8:ex2 T λt4:T.eq T t3 (THead (Flat Appl) w t4) λt4:T.subst0 (s (Flat Appl) i) u0 v t4 ⇒
the thesis becomes ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
we proceed by induction on H8 to prove ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case ex_intro2 : x:T H9:eq T t3 (THead (Flat Appl) w x) H10:subst0 (s (Flat Appl) i) u0 v x ⇒
the thesis becomes ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
(h1)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c w c3 w
by (H1 . . . . previous . H7)
ty3 g c3 w u
end of h1
(h2)
consider H10
we proved subst0 (s (Flat Appl) i) u0 v x
that is equivalent to subst0 i u0 v x
by (fsubst0_both . . . . . previous . H6)
we proved fsubst0 i u0 c v c3 x
by (H3 . . . . previous . H7)
ty3 g c3 x (THead (Bind Abst) u t0)
end of h2
by (ty3_appl . . . . h1 . . h2)
we proved
ty3
g
c3
THead (Flat Appl) w x
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (eq_ind_r . . . previous . H9)
ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case or3_intro2 : H8:ex3_2 T T λu2:T.λt4:T.eq T t3 (THead (Flat Appl) u2 t4) λu2:T.λ:T.subst0 i u0 w u2 λ:T.λt4:T.subst0 (s (Flat Appl) i) u0 v t4 ⇒
the thesis becomes ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
we proceed by induction on H8 to prove ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case ex3_2_intro : x0:T x1:T H9:eq T t3 (THead (Flat Appl) x0 x1) H10:subst0 i u0 w x0 H11:subst0 (s (Flat Appl) i) u0 v x1 ⇒
the thesis becomes ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c v c3 v
by (H3 . . . . previous . H7)
we proved ty3 g c3 v (THead (Bind Abst) u t0)
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c3 (THead (Bind Abst) u t0) t
we proceed by induction on the previous result to prove
ty3
g
c3
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex_intro : x:T H12:ty3 g c3 (THead (Bind Abst) u t0) x ⇒
the thesis becomes
ty3
g
c3
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (ty3_gen_bind . . . . . . H12)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c3 (THead (Bind Abst) u t2) x
λ:T.λt:T.ty3 g c3 u t
λt2:T.λ:T.ty3 g (CHead c3 (Bind Abst) u) t0 t2
we proceed by induction on the previous result to prove
ty3
g
c3
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex3_2_intro : x2:T x3:T :pc3 c3 (THead (Bind Abst) u x2) x :ty3 g c3 u x3 H15:ty3 g (CHead c3 (Bind Abst) u) t0 x2 ⇒
the thesis becomes
ty3
g
c3
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c w c3 w
by (H1 . . . . previous . H7)
we proved ty3 g c3 w u
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c3 u t
we proceed by induction on the previous result to prove
ty3
g
c3
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
case ex_intro : x4:T H16:ty3 g c3 u x4 ⇒
the thesis becomes
ty3
g
c3
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
(h1)
(h1)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u0 c w c3 w
by (H1 . . . . previous . H7)
ty3 g c3 w u
end of h1
(h2)
by (ty3_bind . . . . H16 . . . H15)
ty3 g c3 (THead (Bind Abst) u t0) (THead (Bind Abst) u x2)
end of h2
by (ty3_appl . . . . h1 . . h2)
ty3
g
c3
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u x2)
end of h1
(h2)
(h1)
by (fsubst0_both . . . . . H10 . H6)
we proved fsubst0 i u0 c w c3 x0
by (H1 . . . . previous . H7)
ty3 g c3 x0 u
end of h1
(h2)
consider H11
we proved subst0 (s (Flat Appl) i) u0 v x1
that is equivalent to subst0 i u0 v x1
by (fsubst0_both . . . . . previous . H6)
we proved fsubst0 i u0 c v c3 x1
by (H3 . . . . previous . H7)
ty3 g c3 x1 (THead (Bind Abst) u t0)
end of h2
by (ty3_appl . . . . h1 . . h2)
ty3
g
c3
THead (Flat Appl) x0 x1
THead (Flat Appl) x0 (THead (Bind Abst) u t0)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3
c
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) w (THead (Bind Abst) u t0)
end of h1
(h2)
by (subst0_fst . . . . H10 . .)
we proved
subst0
i
u0
THead (Flat Appl) w (THead (Bind Abst) u t0)
THead (Flat Appl) x0 (THead (Bind Abst) u t0)
by (fsubst0_both . . . . . previous . H6)
fsubst0
i
u0
c
THead (Flat Appl) w (THead (Bind Abst) u t0)
c3
THead (Flat Appl) x0 (THead (Bind Abst) u t0)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H7)
pc3
c3
THead (Flat Appl) x0 (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
c3
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c3
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
ty3
g
c3
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
we proved
ty3
g
c3
THead (Flat Appl) x0 x1
THead (Flat Appl) w (THead (Bind Abst) u t0)
by (eq_ind_r . . . previous . H9)
ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
we proved ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
∀e:C
.∀H7:getl i c (CHead e (Bind Abbr) u0)
.ty3 g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))
we proved
∀e:C
.getl i c (CHead e (Bind Abbr) u0)
→ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
∀i:nat
.∀u0:T
.∀c2:C
.∀t2:T
.∀H4:fsubst0 i u0 c (THead (Flat Appl) w v) c2 t2
.∀e:C
.getl i c (CHead e (Bind Abbr) u0)
→ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
case ty3_cast : c:C t2:T t3:T H0:ty3 g c t2 t3 t0:T H2:ty3 g c t3 t0 ⇒
the thesis becomes
∀i:nat
.∀u:T
.∀c2:C
.∀t4:T
.∀H4:fsubst0 i u c (THead (Flat Cast) t3 t2) c2 t4
.∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c2 t4 (THead (Flat Cast) t0 t3)
(H1) by induction hypothesis we know
∀i:nat
.∀u:T
.∀c2:C.∀t4:T.(fsubst0 i u c t2 c2 t4)→∀e:C.(getl i c (CHead e (Bind Abbr) u))→(ty3 g c2 t4 t3)
(H3) by induction hypothesis we know
∀i:nat
.∀u:T
.∀c2:C.∀t4:T.(fsubst0 i u c t3 c2 t4)→∀e:C.(getl i c (CHead e (Bind Abbr) u))→(ty3 g c2 t4 t0)
assume i: nat
assume u: T
assume c2: C
assume t4: T
suppose H4: fsubst0 i u c (THead (Flat Cast) t3 t2) c2 t4
we proceed by induction on H4 to prove
∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c2 t4 (THead (Flat Cast) t0 t3)
case fsubst0_snd : t5:T H5:subst0 i u (THead (Flat Cast) t3 t2) t5 ⇒
the thesis becomes
∀e:C
.∀H6:(getl i c (CHead e (Bind Abbr) u)).(ty3 g c t5 (THead (Flat Cast) t0 t3))
assume e: C
suppose H6: getl i c (CHead e (Bind Abbr) u)
by (subst0_gen_head . . . . . . H5)
we proved
or3
ex2 T λu2:T.eq T t5 (THead (Flat Cast) u2 t2) λu2:T.subst0 i u t3 u2
ex2 T λt2:T.eq T t5 (THead (Flat Cast) t3 t2) λt2:T.subst0 (s (Flat Cast) i) u t2 t2
ex3_2
T
T
λu2:T.λt2:T.eq T t5 (THead (Flat Cast) u2 t2)
λu2:T.λ:T.subst0 i u t3 u2
λ:T.λt2:T.subst0 (s (Flat Cast) i) u t2 t2
we proceed by induction on the previous result to prove ty3 g c t5 (THead (Flat Cast) t0 t3)
case or3_intro0 : H7:ex2 T λu2:T.eq T t5 (THead (Flat Cast) u2 t2) λu2:T.subst0 i u t3 u2 ⇒
the thesis becomes ty3 g c t5 (THead (Flat Cast) t0 t3)
we proceed by induction on H7 to prove ty3 g c t5 (THead (Flat Cast) t0 t3)
case ex_intro2 : x:T H8:eq T t5 (THead (Flat Cast) x t2) H9:subst0 i u t3 x ⇒
the thesis becomes ty3 g c t5 (THead (Flat Cast) t0 t3)
by (fsubst0_snd . . . . . H9)
we proved fsubst0 i u c t3 c x
by (H3 . . . . previous . H6)
we proved ty3 g c x t0
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c t0 t
we proceed by induction on the previous result to prove ty3 g c (THead (Flat Cast) x t2) (THead (Flat Cast) t0 t3)
case ex_intro : x0:T H10:ty3 g c t0 x0 ⇒
the thesis becomes ty3 g c (THead (Flat Cast) x t2) (THead (Flat Cast) t0 t3)
(h1)
by (ty3_cast . . . . H2 . H10)
ty3 g c (THead (Flat Cast) t0 t3) (THead (Flat Cast) x0 t0)
end of h1
(h2)
(h1)
(h1)
by (fsubst0_snd . . . . . H9)
we proved fsubst0 i u c t3 c x
by (H3 . . . . previous . H6)
ty3 g c x t0
end of h1
(h2)
(h1) by (pc3_refl . .) we proved pc3 c t3 t3
(h2)
by (fsubst0_snd . . . . . H9)
fsubst0 i u c t3 c x
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H6)
we proved pc3 c x t3
by (pc3_s . . . previous)
pc3 c t3 x
end of h2
by (ty3_conv . . . . h1 . . H0 h2)
ty3 g c t2 x
end of h1
(h2)
by (fsubst0_snd . . . . . H9)
we proved fsubst0 i u c t3 c x
by (H3 . . . . previous . H6)
ty3 g c x t0
end of h2
by (ty3_cast . . . . h1 . h2)
ty3 g c (THead (Flat Cast) x t2) (THead (Flat Cast) t0 x)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3 c (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 t3)
end of h1
(h2)
consider H9
we proved subst0 i u t3 x
that is equivalent to subst0 (s (Flat Cast) i) u t3 x
by (subst0_snd . . . . . previous .)
we proved subst0 i u (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 x)
by (fsubst0_snd . . . . . previous)
fsubst0 i u c (THead (Flat Cast) t0 t3) c (THead (Flat Cast) t0 x)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H6)
pc3 c (THead (Flat Cast) t0 x) (THead (Flat Cast) t0 t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c (THead (Flat Cast) x t2) (THead (Flat Cast) t0 t3)
we proved ty3 g c (THead (Flat Cast) x t2) (THead (Flat Cast) t0 t3)
by (eq_ind_r . . . previous . H8)
ty3 g c t5 (THead (Flat Cast) t0 t3)
ty3 g c t5 (THead (Flat Cast) t0 t3)
case or3_intro1 : H7:ex2 T λt6:T.eq T t5 (THead (Flat Cast) t3 t6) λt6:T.subst0 (s (Flat Cast) i) u t2 t6 ⇒
the thesis becomes ty3 g c t5 (THead (Flat Cast) t0 t3)
we proceed by induction on H7 to prove ty3 g c t5 (THead (Flat Cast) t0 t3)
case ex_intro2 : x:T H8:eq T t5 (THead (Flat Cast) t3 x) H9:subst0 (s (Flat Cast) i) u t2 x ⇒
the thesis becomes ty3 g c t5 (THead (Flat Cast) t0 t3)
(h1)
by (fsubst0_snd . . . . . H9)
fsubst0 (s (Flat Cast) i) u c t2 c x
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u)
getl (s (Flat Cast) i) c (CHead e (Bind Abbr) u)
end of h2
by (H1 . . . . h1 . h2)
we proved ty3 g c x t3
by (ty3_cast . . . . previous . H2)
we proved ty3 g c (THead (Flat Cast) t3 x) (THead (Flat Cast) t0 t3)
by (eq_ind_r . . . previous . H8)
ty3 g c t5 (THead (Flat Cast) t0 t3)
ty3 g c t5 (THead (Flat Cast) t0 t3)
case or3_intro2 : H7:ex3_2 T T λu2:T.λt6:T.eq T t5 (THead (Flat Cast) u2 t6) λu2:T.λ:T.subst0 i u t3 u2 λ:T.λt6:T.subst0 (s (Flat Cast) i) u t2 t6 ⇒
the thesis becomes ty3 g c t5 (THead (Flat Cast) t0 t3)
we proceed by induction on H7 to prove ty3 g c t5 (THead (Flat Cast) t0 t3)
case ex3_2_intro : x0:T x1:T H8:eq T t5 (THead (Flat Cast) x0 x1) H9:subst0 i u t3 x0 H10:subst0 (s (Flat Cast) i) u t2 x1 ⇒
the thesis becomes ty3 g c t5 (THead (Flat Cast) t0 t3)
by (fsubst0_snd . . . . . H9)
we proved fsubst0 i u c t3 c x0
by (H3 . . . . previous . H6)
we proved ty3 g c x0 t0
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c t0 t
we proceed by induction on the previous result to prove ty3 g c (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0 t3)
case ex_intro : x:T H11:ty3 g c t0 x ⇒
the thesis becomes ty3 g c (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0 t3)
(h1)
by (ty3_cast . . . . H2 . H11)
ty3 g c (THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0)
end of h1
(h2)
(h1)
(h1)
by (fsubst0_snd . . . . . H9)
we proved fsubst0 i u c t3 c x0
by (H3 . . . . previous . H6)
ty3 g c x0 t0
end of h1
(h2)
(h1)
by (fsubst0_snd . . . . . H10)
fsubst0 (s (Flat Cast) i) u c t2 c x1
end of h1
(h2)
consider H6
we proved getl i c (CHead e (Bind Abbr) u)
getl (s (Flat Cast) i) c (CHead e (Bind Abbr) u)
end of h2
by (H1 . . . . h1 . h2)
ty3 g c x1 t3
end of h2
(h3)
(h1) by (pc3_refl . .) we proved pc3 c t3 t3
(h2)
by (fsubst0_snd . . . . . H9)
fsubst0 i u c t3 c x0
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H6)
we proved pc3 c x0 t3
by (pc3_s . . . previous)
pc3 c t3 x0
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c x1 x0
end of h1
(h2)
by (fsubst0_snd . . . . . H9)
we proved fsubst0 i u c t3 c x0
by (H3 . . . . previous . H6)
ty3 g c x0 t0
end of h2
by (ty3_cast . . . . h1 . h2)
ty3 g c (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0 x0)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3 c (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 t3)
end of h1
(h2)
consider H9
we proved subst0 i u t3 x0
that is equivalent to subst0 (s (Flat Cast) i) u t3 x0
by (subst0_snd . . . . . previous .)
we proved subst0 i u (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 x0)
by (fsubst0_snd . . . . . previous)
fsubst0 i u c (THead (Flat Cast) t0 t3) c (THead (Flat Cast) t0 x0)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H6)
pc3 c (THead (Flat Cast) t0 x0) (THead (Flat Cast) t0 t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0 t3)
we proved ty3 g c (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0 t3)
by (eq_ind_r . . . previous . H8)
ty3 g c t5 (THead (Flat Cast) t0 t3)
ty3 g c t5 (THead (Flat Cast) t0 t3)
we proved ty3 g c t5 (THead (Flat Cast) t0 t3)
∀e:C
.∀H6:(getl i c (CHead e (Bind Abbr) u)).(ty3 g c t5 (THead (Flat Cast) t0 t3))
case fsubst0_fst : c3:C H5:csubst0 i u c c3 ⇒
the thesis becomes
∀e:C
.∀H6:getl i c (CHead e (Bind Abbr) u)
.ty3 g c3 (THead (Flat Cast) t3 t2) (THead (Flat Cast) t0 t3)
assume e: C
suppose H6: getl i c (CHead e (Bind Abbr) u)
(h1)
by (fsubst0_fst . . . . . H5)
we proved fsubst0 i u c t2 c3 t2
by (H1 . . . . previous . H6)
ty3 g c3 t2 t3
end of h1
(h2)
by (fsubst0_fst . . . . . H5)
we proved fsubst0 i u c t3 c3 t3
by (H3 . . . . previous . H6)
ty3 g c3 t3 t0
end of h2
by (ty3_cast . . . . h1 . h2)
we proved ty3 g c3 (THead (Flat Cast) t3 t2) (THead (Flat Cast) t0 t3)
∀e:C
.∀H6:getl i c (CHead e (Bind Abbr) u)
.ty3 g c3 (THead (Flat Cast) t3 t2) (THead (Flat Cast) t0 t3)
case fsubst0_both : t5:T H5:subst0 i u (THead (Flat Cast) t3 t2) t5 c3:C H6:csubst0 i u c c3 ⇒
the thesis becomes
∀e:C.∀H7:(getl i c (CHead e (Bind Abbr) u)).(ty3 g c3 t5 (THead (Flat Cast) t0 t3))
assume e: C
suppose H7: getl i c (CHead e (Bind Abbr) u)
by (subst0_gen_head . . . . . . H5)
we proved
or3
ex2 T λu2:T.eq T t5 (THead (Flat Cast) u2 t2) λu2:T.subst0 i u t3 u2
ex2 T λt2:T.eq T t5 (THead (Flat Cast) t3 t2) λt2:T.subst0 (s (Flat Cast) i) u t2 t2
ex3_2
T
T
λu2:T.λt2:T.eq T t5 (THead (Flat Cast) u2 t2)
λu2:T.λ:T.subst0 i u t3 u2
λ:T.λt2:T.subst0 (s (Flat Cast) i) u t2 t2
we proceed by induction on the previous result to prove ty3 g c3 t5 (THead (Flat Cast) t0 t3)
case or3_intro0 : H8:ex2 T λu2:T.eq T t5 (THead (Flat Cast) u2 t2) λu2:T.subst0 i u t3 u2 ⇒
the thesis becomes ty3 g c3 t5 (THead (Flat Cast) t0 t3)
we proceed by induction on H8 to prove ty3 g c3 t5 (THead (Flat Cast) t0 t3)
case ex_intro2 : x:T H9:eq T t5 (THead (Flat Cast) x t2) H10:subst0 i u t3 x ⇒
the thesis becomes ty3 g c3 t5 (THead (Flat Cast) t0 t3)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u c t3 c3 t3
by (H3 . . . . previous . H7)
we proved ty3 g c3 t3 t0
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c3 t0 t
we proceed by induction on the previous result to prove ty3 g c3 (THead (Flat Cast) x t2) (THead (Flat Cast) t0 t3)
case ex_intro : x0:T H11:ty3 g c3 t0 x0 ⇒
the thesis becomes ty3 g c3 (THead (Flat Cast) x t2) (THead (Flat Cast) t0 t3)
(h1)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u c t3 c3 t3
by (H3 . . . . previous . H7)
we proved ty3 g c3 t3 t0
by (ty3_cast . . . . previous . H11)
ty3 g c3 (THead (Flat Cast) t0 t3) (THead (Flat Cast) x0 t0)
end of h1
(h2)
(h1)
(h1)
by (fsubst0_both . . . . . H10 . H6)
we proved fsubst0 i u c t3 c3 x
by (H3 . . . . previous . H7)
ty3 g c3 x t0
end of h1
(h2)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u c t2 c3 t2
by (H1 . . . . previous . H7)
ty3 g c3 t2 t3
end of h2
(h3)
(h1) by (pc3_refl . .) we proved pc3 c t3 t3
(h2)
by (fsubst0_both . . . . . H10 . H6)
fsubst0 i u c t3 c3 x
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H7)
we proved pc3 c3 x t3
by (pc3_s . . . previous)
pc3 c3 t3 x
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c3 t2 x
end of h1
(h2)
by (fsubst0_both . . . . . H10 . H6)
we proved fsubst0 i u c t3 c3 x
by (H3 . . . . previous . H7)
ty3 g c3 x t0
end of h2
by (ty3_cast . . . . h1 . h2)
ty3 g c3 (THead (Flat Cast) x t2) (THead (Flat Cast) t0 x)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3 c (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 t3)
end of h1
(h2)
consider H10
we proved subst0 i u t3 x
that is equivalent to subst0 (s (Flat Cast) i) u t3 x
by (subst0_snd . . . . . previous .)
we proved subst0 i u (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 x)
by (fsubst0_both . . . . . previous . H6)
fsubst0 i u c (THead (Flat Cast) t0 t3) c3 (THead (Flat Cast) t0 x)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H7)
pc3 c3 (THead (Flat Cast) t0 x) (THead (Flat Cast) t0 t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c3 (THead (Flat Cast) x t2) (THead (Flat Cast) t0 t3)
we proved ty3 g c3 (THead (Flat Cast) x t2) (THead (Flat Cast) t0 t3)
by (eq_ind_r . . . previous . H9)
ty3 g c3 t5 (THead (Flat Cast) t0 t3)
ty3 g c3 t5 (THead (Flat Cast) t0 t3)
case or3_intro1 : H8:ex2 T λt6:T.eq T t5 (THead (Flat Cast) t3 t6) λt6:T.subst0 (s (Flat Cast) i) u t2 t6 ⇒
the thesis becomes ty3 g c3 t5 (THead (Flat Cast) t0 t3)
we proceed by induction on H8 to prove ty3 g c3 t5 (THead (Flat Cast) t0 t3)
case ex_intro2 : x:T H9:eq T t5 (THead (Flat Cast) t3 x) H10:subst0 (s (Flat Cast) i) u t2 x ⇒
the thesis becomes ty3 g c3 t5 (THead (Flat Cast) t0 t3)
(h1)
consider H10
we proved subst0 (s (Flat Cast) i) u t2 x
that is equivalent to subst0 i u t2 x
by (fsubst0_both . . . . . previous . H6)
we proved fsubst0 i u c t2 c3 x
by (H1 . . . . previous . H7)
ty3 g c3 x t3
end of h1
(h2)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u c t3 c3 t3
by (H3 . . . . previous . H7)
ty3 g c3 t3 t0
end of h2
by (ty3_cast . . . . h1 . h2)
we proved ty3 g c3 (THead (Flat Cast) t3 x) (THead (Flat Cast) t0 t3)
by (eq_ind_r . . . previous . H9)
ty3 g c3 t5 (THead (Flat Cast) t0 t3)
ty3 g c3 t5 (THead (Flat Cast) t0 t3)
case or3_intro2 : H8:ex3_2 T T λu2:T.λt6:T.eq T t5 (THead (Flat Cast) u2 t6) λu2:T.λ:T.subst0 i u t3 u2 λ:T.λt6:T.subst0 (s (Flat Cast) i) u t2 t6 ⇒
the thesis becomes ty3 g c3 t5 (THead (Flat Cast) t0 t3)
we proceed by induction on H8 to prove ty3 g c3 t5 (THead (Flat Cast) t0 t3)
case ex3_2_intro : x0:T x1:T H9:eq T t5 (THead (Flat Cast) x0 x1) H10:subst0 i u t3 x0 H11:subst0 (s (Flat Cast) i) u t2 x1 ⇒
the thesis becomes ty3 g c3 t5 (THead (Flat Cast) t0 t3)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u c t3 c3 t3
by (H3 . . . . previous . H7)
we proved ty3 g c3 t3 t0
by (ty3_correct . . . . previous)
we proved ex T λt:T.ty3 g c3 t0 t
we proceed by induction on the previous result to prove ty3 g c3 (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0 t3)
case ex_intro : x:T H12:ty3 g c3 t0 x ⇒
the thesis becomes ty3 g c3 (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0 t3)
(h1)
by (fsubst0_fst . . . . . H6)
we proved fsubst0 i u c t3 c3 t3
by (H3 . . . . previous . H7)
we proved ty3 g c3 t3 t0
by (ty3_cast . . . . previous . H12)
ty3 g c3 (THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0)
end of h1
(h2)
(h1)
(h1)
by (fsubst0_both . . . . . H10 . H6)
we proved fsubst0 i u c t3 c3 x0
by (H3 . . . . previous . H7)
ty3 g c3 x0 t0
end of h1
(h2)
consider H11
we proved subst0 (s (Flat Cast) i) u t2 x1
that is equivalent to subst0 i u t2 x1
by (fsubst0_both . . . . . previous . H6)
we proved fsubst0 i u c t2 c3 x1
by (H1 . . . . previous . H7)
ty3 g c3 x1 t3
end of h2
(h3)
(h1) by (pc3_refl . .) we proved pc3 c t3 t3
(h2)
by (fsubst0_both . . . . . H10 . H6)
fsubst0 i u c t3 c3 x0
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H7)
we proved pc3 c3 x0 t3
by (pc3_s . . . previous)
pc3 c3 t3 x0
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c3 x1 x0
end of h1
(h2)
by (fsubst0_both . . . . . H10 . H6)
we proved fsubst0 i u c t3 c3 x0
by (H3 . . . . previous . H7)
ty3 g c3 x0 t0
end of h2
by (ty3_cast . . . . h1 . h2)
ty3 g c3 (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0 x0)
end of h2
(h3)
(h1)
by (pc3_refl . .)
pc3 c (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 t3)
end of h1
(h2)
consider H10
we proved subst0 i u t3 x0
that is equivalent to subst0 (s (Flat Cast) i) u t3 x0
by (subst0_snd . . . . . previous .)
we proved subst0 i u (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 x0)
by (fsubst0_both . . . . . previous . H6)
fsubst0 i u c (THead (Flat Cast) t0 t3) c3 (THead (Flat Cast) t0 x0)
end of h2
by (pc3_fsubst0 . . . h1 . . . . h2 . H7)
pc3 c3 (THead (Flat Cast) t0 x0) (THead (Flat Cast) t0 t3)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c3 (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0 t3)
we proved ty3 g c3 (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0 t3)
by (eq_ind_r . . . previous . H9)
ty3 g c3 t5 (THead (Flat Cast) t0 t3)
ty3 g c3 t5 (THead (Flat Cast) t0 t3)
we proved ty3 g c3 t5 (THead (Flat Cast) t0 t3)
∀e:C.∀H7:(getl i c (CHead e (Bind Abbr) u)).(ty3 g c3 t5 (THead (Flat Cast) t0 t3))
we proved
∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c2 t4 (THead (Flat Cast) t0 t3)
∀i:nat
.∀u:T
.∀c2:C
.∀t4:T
.∀H4:fsubst0 i u c (THead (Flat Cast) t3 t2) c2 t4
.∀e:C
.getl i c (CHead e (Bind Abbr) u)
→ty3 g c2 t4 (THead (Flat Cast) t0 t3)
we proved
∀i:nat
.∀u:T.∀c2:C.∀t3:T.(fsubst0 i u c1 t1 c2 t3)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(ty3 g c2 t3 t)
we proved
∀g:G
.∀c1:C
.∀t1:T
.∀t:T
.ty3 g c1 t1 t
→∀i:nat
.∀u:T.∀c2:C.∀t3:T.(fsubst0 i u c1 t1 c2 t3)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(ty3 g c2 t3 t)