DEFINITION ty3_getl_subst0()
TYPE =
∀g:G
.∀c:C
.∀t:T
.∀u:T
.ty3 g c t u
→∀v0:T
.∀t0:T
.∀i:nat
.subst0 i v0 t t0
→∀b:B.∀d:C.∀v:T.(getl i c (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)
BODY =
assume g: G
assume c: C
assume t: T
assume u: T
suppose H: ty3 g c t u
we proceed by induction on H to prove
∀v0:T
.∀t2:T
.∀i:nat
.subst0 i v0 t t2
→∀b:B.∀d:C.∀v:T.(getl i c (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)
case ty3_conv : c0:C t2:T t0:T :ty3 g c0 t2 t0 u0:T t1:T :ty3 g c0 u0 t1 :pc3 c0 t1 t2 ⇒
the thesis becomes
∀v0:T
.∀t3:T
.∀i:nat.∀H5:(subst0 i v0 u0 t3).∀b:B.∀d:C.∀v:T.∀H6:(getl i c0 (CHead d (Bind b) v)).(ex T λw:T.ty3 g d v w)
() by induction hypothesis we know
∀v0:T
.∀t1:T
.∀i:nat
.subst0 i v0 t2 t1
→∀b:B.∀d:C.∀v:T.(getl i c0 (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)
(H3) by induction hypothesis we know
∀v0:T
.∀t3:T
.∀i:nat
.subst0 i v0 u0 t3
→∀b:B.∀d:C.∀v:T.(getl i c0 (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)
assume v0: T
assume t3: T
assume i: nat
suppose H5: subst0 i v0 u0 t3
assume b: B
assume d: C
assume v: T
suppose H6: getl i c0 (CHead d (Bind b) v)
by (H3 . . . H5 . . . H6)
we proved ex T λw:T.ty3 g d v w
∀v0:T
.∀t3:T
.∀i:nat.∀H5:(subst0 i v0 u0 t3).∀b:B.∀d:C.∀v:T.∀H6:(getl i c0 (CHead d (Bind b) v)).(ex T λw:T.ty3 g d v w)
case ty3_sort : c0:C m:nat ⇒
the thesis becomes
∀v0:T
.∀t0:T
.∀i:nat
.∀H0:subst0 i v0 (TSort m) t0
.∀b:B.∀d:C.∀v:T.(getl i c0 (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)
assume v0: T
assume t0: T
assume i: nat
suppose H0: subst0 i v0 (TSort m) t0
assume b: B
assume d: C
assume v: T
suppose : getl i c0 (CHead d (Bind b) v)
by (subst0_gen_sort . . . . H0 .)
we proved ex T λw:T.ty3 g d v w
∀v0:T
.∀t0:T
.∀i:nat
.∀H0:subst0 i v0 (TSort m) t0
.∀b:B.∀d:C.∀v:T.(getl i c0 (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)
case ty3_abbr : n:nat c0:C d:C u0:T H0:getl n c0 (CHead d (Bind Abbr) u0) t0:T H1:ty3 g d u0 t0 ⇒
the thesis becomes
∀v0:T
.∀t1:T
.∀i:nat
.∀H3:subst0 i v0 (TLRef n) t1
.∀b:B.∀d0:C.∀v:T.∀H4:(getl i c0 (CHead d0 (Bind b) v)).(ex T λw:T.ty3 g d0 v w)
() by induction hypothesis we know
∀v0:T
.∀t1:T
.∀i:nat
.subst0 i v0 u0 t1
→∀b:B.∀d0:C.∀v:T.(getl i d (CHead d0 (Bind b) v))→(ex T λw:T.ty3 g d0 v w)
assume v0: T
assume t1: T
assume i: nat
suppose H3: subst0 i v0 (TLRef n) t1
assume b: B
assume d0: C
assume v: T
suppose H4: getl i c0 (CHead d0 (Bind b) v)
by (subst0_gen_lref . . . . H3)
we proved land (eq nat n i) (eq T t1 (lift (S n) O v0))
we proceed by induction on the previous result to prove ex T λw:T.ty3 g d0 v w
case conj : H5:eq nat n i :eq T t1 (lift (S n) O v0) ⇒
the thesis becomes ex T λw:T.ty3 g d0 v w
(H7)
by (eq_ind_r . . . H4 . H5)
getl n c0 (CHead d0 (Bind b) v)
end of H7
(H8)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v)
we proceed by induction on the previous result to prove getl n c0 (CHead d0 (Bind b) v)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl n c0 (CHead d0 (Bind b) v)
end of H8
(H9)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u0 OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead d0 (Bind b) v OF CSort ⇒d | CHead c1 ⇒c1
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead d (Bind Abbr) u0)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead d0 (Bind b) v)
end of H9
(h1)
(H10)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u0 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead d0 (Bind b) v OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
CHead d (Bind Abbr) u0
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
CHead d0 (Bind b) v
end of H10
(h1)
(H11)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u0 OF CSort ⇒u0 | CHead t2⇒t2
<λ:C.T> CASE CHead d0 (Bind b) v OF CSort ⇒u0 | CHead t2⇒t2
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t2⇒t2 (CHead d (Bind Abbr) u0)
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t2⇒t2 (CHead d0 (Bind b) v)
end of H11
suppose H12: eq B Abbr b
suppose H13: eq C d d0
(H14)
consider H11
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u0 OF CSort ⇒u0 | CHead t2⇒t2
<λ:C.T> CASE CHead d0 (Bind b) v OF CSort ⇒u0 | CHead t2⇒t2
that is equivalent to eq T u0 v
by (eq_ind_r . . . H8 . previous)
getl n c0 (CHead d0 (Bind b) u0)
end of H14
consider H11
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u0 OF CSort ⇒u0 | CHead t2⇒t2
<λ:C.T> CASE CHead d0 (Bind b) v OF CSort ⇒u0 | CHead t2⇒t2
that is equivalent to eq T u0 v
we proceed by induction on the previous result to prove ex T λw:T.ty3 g d0 v w
case refl_equal : ⇒
the thesis becomes ex T λw:T.ty3 g d0 u0 w
(H15)
by (eq_ind_r . . . H14 . H13)
getl n c0 (CHead d (Bind b) u0)
end of H15
we proceed by induction on H13 to prove ex T λw:T.ty3 g d0 u0 w
case refl_equal : ⇒
the thesis becomes ex T λw:T.ty3 g d u0 w
by (ex_intro . . . H1)
ex T λw:T.ty3 g d u0 w
ex T λw:T.ty3 g d0 u0 w
we proved ex T λw:T.ty3 g d0 v w
(eq B Abbr b)→(eq C d d0)→(ex T λw:T.ty3 g d0 v w)
end of h1
(h2)
consider H10
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u0 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead d0 (Bind b) v OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
eq B Abbr b
end of h2
by (h1 h2)
(eq C d d0)→(ex T λw:T.ty3 g d0 v w)
end of h1
(h2)
consider H9
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u0 OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead d0 (Bind b) v OF CSort ⇒d | CHead c1 ⇒c1
eq C d d0
end of h2
by (h1 h2)
ex T λw:T.ty3 g d0 v w
we proved ex T λw:T.ty3 g d0 v w
∀v0:T
.∀t1:T
.∀i:nat
.∀H3:subst0 i v0 (TLRef n) t1
.∀b:B.∀d0:C.∀v:T.∀H4:(getl i c0 (CHead d0 (Bind b) v)).(ex T λw:T.ty3 g d0 v w)
case ty3_abst : n:nat c0:C d:C u0:T H0:getl n c0 (CHead d (Bind Abst) u0) t0:T H1:ty3 g d u0 t0 ⇒
the thesis becomes
∀v0:T
.∀t1:T
.∀i:nat
.∀H3:subst0 i v0 (TLRef n) t1
.∀b:B.∀d0:C.∀v:T.∀H4:(getl i c0 (CHead d0 (Bind b) v)).(ex T λw:T.ty3 g d0 v w)
() by induction hypothesis we know
∀v0:T
.∀t1:T
.∀i:nat
.subst0 i v0 u0 t1
→∀b:B.∀d0:C.∀v:T.(getl i d (CHead d0 (Bind b) v))→(ex T λw:T.ty3 g d0 v w)
assume v0: T
assume t1: T
assume i: nat
suppose H3: subst0 i v0 (TLRef n) t1
assume b: B
assume d0: C
assume v: T
suppose H4: getl i c0 (CHead d0 (Bind b) v)
by (subst0_gen_lref . . . . H3)
we proved land (eq nat n i) (eq T t1 (lift (S n) O v0))
we proceed by induction on the previous result to prove ex T λw:T.ty3 g d0 v w
case conj : H5:eq nat n i :eq T t1 (lift (S n) O v0) ⇒
the thesis becomes ex T λw:T.ty3 g d0 v w
(H7)
by (eq_ind_r . . . H4 . H5)
getl n c0 (CHead d0 (Bind b) v)
end of H7
(H8)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abst) u0) (CHead d0 (Bind b) v)
we proceed by induction on the previous result to prove getl n c0 (CHead d0 (Bind b) v)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl n c0 (CHead d0 (Bind b) v)
end of H8
(H9)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abst) u0) (CHead d0 (Bind b) v)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u0 OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead d0 (Bind b) v OF CSort ⇒d | CHead c1 ⇒c1
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead d (Bind Abst) u0)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead d0 (Bind b) v)
end of H9
(h1)
(H10)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abst) u0) (CHead d0 (Bind b) v)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u0 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
<λ:C.B>
CASE CHead d0 (Bind b) v OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
CHead d (Bind Abst) u0
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
CHead d0 (Bind b) v
end of H10
(h1)
(H11)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abst) u0) (CHead d0 (Bind b) v)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u0 OF CSort ⇒u0 | CHead t2⇒t2
<λ:C.T> CASE CHead d0 (Bind b) v OF CSort ⇒u0 | CHead t2⇒t2
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t2⇒t2 (CHead d (Bind Abst) u0)
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t2⇒t2 (CHead d0 (Bind b) v)
end of H11
suppose H12: eq B Abst b
suppose H13: eq C d d0
(H14)
consider H11
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u0 OF CSort ⇒u0 | CHead t2⇒t2
<λ:C.T> CASE CHead d0 (Bind b) v OF CSort ⇒u0 | CHead t2⇒t2
that is equivalent to eq T u0 v
by (eq_ind_r . . . H8 . previous)
getl n c0 (CHead d0 (Bind b) u0)
end of H14
consider H11
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u0 OF CSort ⇒u0 | CHead t2⇒t2
<λ:C.T> CASE CHead d0 (Bind b) v OF CSort ⇒u0 | CHead t2⇒t2
that is equivalent to eq T u0 v
we proceed by induction on the previous result to prove ex T λw:T.ty3 g d0 v w
case refl_equal : ⇒
the thesis becomes ex T λw:T.ty3 g d0 u0 w
(H15)
by (eq_ind_r . . . H14 . H13)
getl n c0 (CHead d (Bind b) u0)
end of H15
we proceed by induction on H13 to prove ex T λw:T.ty3 g d0 u0 w
case refl_equal : ⇒
the thesis becomes ex T λw:T.ty3 g d u0 w
by (ex_intro . . . H1)
ex T λw:T.ty3 g d u0 w
ex T λw:T.ty3 g d0 u0 w
we proved ex T λw:T.ty3 g d0 v w
(eq B Abst b)→(eq C d d0)→(ex T λw:T.ty3 g d0 v w)
end of h1
(h2)
consider H10
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u0 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
<λ:C.B>
CASE CHead d0 (Bind b) v OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
eq B Abst b
end of h2
by (h1 h2)
(eq C d d0)→(ex T λw:T.ty3 g d0 v w)
end of h1
(h2)
consider H9
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u0 OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead d0 (Bind b) v OF CSort ⇒d | CHead c1 ⇒c1
eq C d d0
end of h2
by (h1 h2)
ex T λw:T.ty3 g d0 v w
we proved ex T λw:T.ty3 g d0 v w
∀v0:T
.∀t1:T
.∀i:nat
.∀H3:subst0 i v0 (TLRef n) t1
.∀b:B.∀d0:C.∀v:T.∀H4:(getl i c0 (CHead d0 (Bind b) v)).(ex T λw:T.ty3 g d0 v w)
case ty3_bind : c0:C u0:T t0:T :ty3 g c0 u0 t0 b:B t1:T t2:T :ty3 g (CHead c0 (Bind b) u0) t1 t2 ⇒
the thesis becomes
∀v0:T
.∀t3:T
.∀i:nat
.∀H4:subst0 i v0 (THead (Bind b) u0 t1) t3
.∀b0:B.∀d:C.∀v:T.∀H5:(getl i c0 (CHead d (Bind b0) v)).(ex T λw:T.ty3 g d v w)
(H1) by induction hypothesis we know
∀v0:T
.∀t1:T
.∀i:nat
.subst0 i v0 u0 t1
→∀b:B.∀d:C.∀v:T.(getl i c0 (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)
(H3) by induction hypothesis we know
∀v0:T
.∀t3:T
.∀i:nat
.subst0 i v0 t1 t3
→∀b0:B
.∀d:C
.∀v:T
.getl i (CHead c0 (Bind b) u0) (CHead d (Bind b0) v)
→ex T λw:T.ty3 g d v w
assume v0: T
assume t3: T
assume i: nat
suppose H4: subst0 i v0 (THead (Bind b) u0 t1) t3
assume b0: B
assume d: C
assume v: T
suppose H5: getl i c0 (CHead d (Bind b0) v)
by (subst0_gen_head . . . . . . H4)
we proved
or3
ex2 T λu2:T.eq T t3 (THead (Bind b) u2 t1) λu2:T.subst0 i v0 u0 u2
ex2 T λt2:T.eq T t3 (THead (Bind b) u0 t2) λt2:T.subst0 (s (Bind b) i) v0 t1 t2
ex3_2 T T λu2:T.λt2:T.eq T t3 (THead (Bind b) u2 t2) λu2:T.λ:T.subst0 i v0 u0 u2 λ:T.λt2:T.subst0 (s (Bind b) i) v0 t1 t2
we proceed by induction on the previous result to prove ex T λw:T.ty3 g d v w
case or3_intro0 : H6:ex2 T λu2:T.eq T t3 (THead (Bind b) u2 t1) λu2:T.subst0 i v0 u0 u2 ⇒
the thesis becomes ex T λw:T.ty3 g d v w
we proceed by induction on H6 to prove ex T λw:T.ty3 g d v w
case ex_intro2 : x:T :eq T t3 (THead (Bind b) x t1) H8:subst0 i v0 u0 x ⇒
the thesis becomes ex T λw:T.ty3 g d v w
by (H1 . . . H8 . . . H5)
ex T λw:T.ty3 g d v w
ex T λw:T.ty3 g d v w
case or3_intro1 : H6:ex2 T λt4:T.eq T t3 (THead (Bind b) u0 t4) λt4:T.subst0 (s (Bind b) i) v0 t1 t4 ⇒
the thesis becomes ex T λw:T.ty3 g d v w
we proceed by induction on H6 to prove ex T λw:T.ty3 g d v w
case ex_intro2 : x:T :eq T t3 (THead (Bind b) u0 x) H8:subst0 (s (Bind b) i) v0 t1 x ⇒
the thesis becomes ex T λw:T.ty3 g d v w
(h1)
consider H8
we proved subst0 (s (Bind b) i) v0 t1 x
subst0 (S i) v0 t1 x
end of h1
(h2)
consider H5
we proved getl i c0 (CHead d (Bind b0) v)
that is equivalent to getl (r (Bind b) i) c0 (CHead d (Bind b0) v)
by (getl_head . . . . previous .)
getl (S i) (CHead c0 (Bind b) u0) (CHead d (Bind b0) v)
end of h2
by (H3 . . . h1 . . . h2)
ex T λw:T.ty3 g d v w
ex T λw:T.ty3 g d v w
case or3_intro2 : H6:ex3_2 T T λu2:T.λt4:T.eq T t3 (THead (Bind b) u2 t4) λu2:T.λ:T.subst0 i v0 u0 u2 λ:T.λt4:T.subst0 (s (Bind b) i) v0 t1 t4 ⇒
the thesis becomes ex T λw:T.ty3 g d v w
we proceed by induction on H6 to prove ex T λw:T.ty3 g d v w
case ex3_2_intro : x0:T x1:T :eq T t3 (THead (Bind b) x0 x1) H8:subst0 i v0 u0 x0 :subst0 (s (Bind b) i) v0 t1 x1 ⇒
the thesis becomes ex T λw:T.ty3 g d v w
by (H1 . . . H8 . . . H5)
ex T λw:T.ty3 g d v w
ex T λw:T.ty3 g d v w
we proved ex T λw:T.ty3 g d v w
∀v0:T
.∀t3:T
.∀i:nat
.∀H4:subst0 i v0 (THead (Bind b) u0 t1) t3
.∀b0:B.∀d:C.∀v:T.∀H5:(getl i c0 (CHead d (Bind b0) v)).(ex T λw:T.ty3 g d v w)
case ty3_appl : c0:C w:T u0:T :ty3 g c0 w u0 v:T t0:T :ty3 g c0 v (THead (Bind Abst) u0 t0) ⇒
the thesis becomes
∀v0:T
.∀t1:T
.∀i:nat
.∀H4:subst0 i v0 (THead (Flat Appl) w v) t1
.∀b:B.∀d:C.∀v1:T.∀H5:(getl i c0 (CHead d (Bind b) v1)).(ex T λw0:T.ty3 g d v1 w0)
(H1) by induction hypothesis we know
∀v0:T
.∀t0:T
.∀i:nat
.subst0 i v0 w t0
→∀b:B.∀d:C.∀v:T.(getl i c0 (CHead d (Bind b) v))→(ex T λw0:T.ty3 g d v w0)
(H3) by induction hypothesis we know
∀v0:T
.∀t1:T
.∀i:nat
.subst0 i v0 v t1
→∀b:B.∀d:C.∀v1:T.(getl i c0 (CHead d (Bind b) v1))→(ex T λw0:T.ty3 g d v1 w0)
assume v0: T
assume t1: T
assume i: nat
suppose H4: subst0 i v0 (THead (Flat Appl) w v) t1
assume b: B
assume d: C
assume v1: T
suppose H5: getl i c0 (CHead d (Bind b) v1)
by (subst0_gen_head . . . . . . H4)
we proved
or3
ex2 T λu2:T.eq T t1 (THead (Flat Appl) u2 v) λu2:T.subst0 i v0 w u2
ex2 T λt2:T.eq T t1 (THead (Flat Appl) w t2) λt2:T.subst0 (s (Flat Appl) i) v0 v t2
ex3_2
T
T
λu2:T.λt2:T.eq T t1 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.subst0 i v0 w u2
λ:T.λt2:T.subst0 (s (Flat Appl) i) v0 v t2
we proceed by induction on the previous result to prove ex T λw0:T.ty3 g d v1 w0
case or3_intro0 : H6:ex2 T λu2:T.eq T t1 (THead (Flat Appl) u2 v) λu2:T.subst0 i v0 w u2 ⇒
the thesis becomes ex T λw0:T.ty3 g d v1 w0
we proceed by induction on H6 to prove ex T λw0:T.ty3 g d v1 w0
case ex_intro2 : x:T :eq T t1 (THead (Flat Appl) x v) H8:subst0 i v0 w x ⇒
the thesis becomes ex T λw0:T.ty3 g d v1 w0
by (H1 . . . H8 . . . H5)
ex T λw0:T.ty3 g d v1 w0
ex T λw0:T.ty3 g d v1 w0
case or3_intro1 : H6:ex2 T λt2:T.eq T t1 (THead (Flat Appl) w t2) λt2:T.subst0 (s (Flat Appl) i) v0 v t2 ⇒
the thesis becomes ex T λw0:T.ty3 g d v1 w0
we proceed by induction on H6 to prove ex T λw0:T.ty3 g d v1 w0
case ex_intro2 : x:T :eq T t1 (THead (Flat Appl) w x) H8:subst0 (s (Flat Appl) i) v0 v x ⇒
the thesis becomes ex T λw0:T.ty3 g d v1 w0
consider H5
we proved getl i c0 (CHead d (Bind b) v1)
that is equivalent to getl (s (Flat Appl) i) c0 (CHead d (Bind b) v1)
by (H3 . . . H8 . . . previous)
ex T λw0:T.ty3 g d v1 w0
ex T λw0:T.ty3 g d v1 w0
case or3_intro2 : H6:ex3_2 T T λu2:T.λt2:T.eq T t1 (THead (Flat Appl) u2 t2) λu2:T.λ:T.subst0 i v0 w u2 λ:T.λt2:T.subst0 (s (Flat Appl) i) v0 v t2 ⇒
the thesis becomes ex T λw0:T.ty3 g d v1 w0
we proceed by induction on H6 to prove ex T λw0:T.ty3 g d v1 w0
case ex3_2_intro : x0:T x1:T :eq T t1 (THead (Flat Appl) x0 x1) :subst0 i v0 w x0 H9:subst0 (s (Flat Appl) i) v0 v x1 ⇒
the thesis becomes ex T λw0:T.ty3 g d v1 w0
consider H5
we proved getl i c0 (CHead d (Bind b) v1)
that is equivalent to getl (s (Flat Appl) i) c0 (CHead d (Bind b) v1)
by (H3 . . . H9 . . . previous)
ex T λw0:T.ty3 g d v1 w0
ex T λw0:T.ty3 g d v1 w0
we proved ex T λw0:T.ty3 g d v1 w0
∀v0:T
.∀t1:T
.∀i:nat
.∀H4:subst0 i v0 (THead (Flat Appl) w v) t1
.∀b:B.∀d:C.∀v1:T.∀H5:(getl i c0 (CHead d (Bind b) v1)).(ex T λw0:T.ty3 g d v1 w0)
case ty3_cast : c0:C t1:T t2:T :ty3 g c0 t1 t2 t0:T :ty3 g c0 t2 t0 ⇒
the thesis becomes
∀v0:T
.∀t3:T
.∀i:nat
.∀H4:subst0 i v0 (THead (Flat Cast) t2 t1) t3
.∀b:B.∀d:C.∀v:T.∀H5:(getl i c0 (CHead d (Bind b) v)).(ex T λw:T.ty3 g d v w)
(H1) by induction hypothesis we know
∀v0:T
.∀t0:T
.∀i:nat
.subst0 i v0 t1 t0
→∀b:B.∀d:C.∀v:T.(getl i c0 (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)
(H3) by induction hypothesis we know
∀v0:T
.∀t3:T
.∀i:nat
.subst0 i v0 t2 t3
→∀b:B.∀d:C.∀v:T.(getl i c0 (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)
assume v0: T
assume t3: T
assume i: nat
suppose H4: subst0 i v0 (THead (Flat Cast) t2 t1) t3
assume b: B
assume d: C
assume v: T
suppose H5: getl i c0 (CHead d (Bind b) v)
by (subst0_gen_head . . . . . . H4)
we proved
or3
ex2 T λu2:T.eq T t3 (THead (Flat Cast) u2 t1) λu2:T.subst0 i v0 t2 u2
ex2 T λt2:T.eq T t3 (THead (Flat Cast) t2 t2) λt2:T.subst0 (s (Flat Cast) i) v0 t1 t2
ex3_2
T
T
λu2:T.λt2:T.eq T t3 (THead (Flat Cast) u2 t2)
λu2:T.λ:T.subst0 i v0 t2 u2
λ:T.λt2:T.subst0 (s (Flat Cast) i) v0 t1 t2
we proceed by induction on the previous result to prove ex T λw:T.ty3 g d v w
case or3_intro0 : H6:ex2 T λu2:T.eq T t3 (THead (Flat Cast) u2 t1) λu2:T.subst0 i v0 t2 u2 ⇒
the thesis becomes ex T λw:T.ty3 g d v w
we proceed by induction on H6 to prove ex T λw:T.ty3 g d v w
case ex_intro2 : x:T :eq T t3 (THead (Flat Cast) x t1) H8:subst0 i v0 t2 x ⇒
the thesis becomes ex T λw:T.ty3 g d v w
by (H3 . . . H8 . . . H5)
ex T λw:T.ty3 g d v w
ex T λw:T.ty3 g d v w
case or3_intro1 : H6:ex2 T λt4:T.eq T t3 (THead (Flat Cast) t2 t4) λt4:T.subst0 (s (Flat Cast) i) v0 t1 t4 ⇒
the thesis becomes ex T λw:T.ty3 g d v w
we proceed by induction on H6 to prove ex T λw:T.ty3 g d v w
case ex_intro2 : x:T :eq T t3 (THead (Flat Cast) t2 x) H8:subst0 (s (Flat Cast) i) v0 t1 x ⇒
the thesis becomes ex T λw:T.ty3 g d v w
consider H5
we proved getl i c0 (CHead d (Bind b) v)
that is equivalent to getl (s (Flat Cast) i) c0 (CHead d (Bind b) v)
by (H1 . . . H8 . . . previous)
ex T λw:T.ty3 g d v w
ex T λw:T.ty3 g d v w
case or3_intro2 : H6:ex3_2 T T λu2:T.λt4:T.eq T t3 (THead (Flat Cast) u2 t4) λu2:T.λ:T.subst0 i v0 t2 u2 λ:T.λt4:T.subst0 (s (Flat Cast) i) v0 t1 t4 ⇒
the thesis becomes ex T λw:T.ty3 g d v w
we proceed by induction on H6 to prove ex T λw:T.ty3 g d v w
case ex3_2_intro : x0:T x1:T :eq T t3 (THead (Flat Cast) x0 x1) H8:subst0 i v0 t2 x0 :subst0 (s (Flat Cast) i) v0 t1 x1 ⇒
the thesis becomes ex T λw:T.ty3 g d v w
by (H3 . . . H8 . . . H5)
ex T λw:T.ty3 g d v w
ex T λw:T.ty3 g d v w
we proved ex T λw:T.ty3 g d v w
∀v0:T
.∀t3:T
.∀i:nat
.∀H4:subst0 i v0 (THead (Flat Cast) t2 t1) t3
.∀b:B.∀d:C.∀v:T.∀H5:(getl i c0 (CHead d (Bind b) v)).(ex T λw:T.ty3 g d v w)
we proved
∀v0:T
.∀t2:T
.∀i:nat
.subst0 i v0 t t2
→∀b:B.∀d:C.∀v:T.(getl i c (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)
we proved
∀g:G
.∀c:C
.∀t:T
.∀u:T
.ty3 g c t u
→∀v0:T
.∀t2:T
.∀i:nat
.subst0 i v0 t t2
→∀b:B.∀d:C.∀v:T.(getl i c (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)