DEFINITION pc3_pr2_fsubst0_back()
TYPE =
∀c1:C
.∀t:T
.∀t1:T
.pr2 c1 t t1
→∀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))→(pc3 c2 t t2)
BODY =
assume c1: C
assume t: T
assume t1: T
suppose H: pr2 c1 t t1
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))→(pc3 c2 t t3)
case pr2_free : c:C t2:T t3:T H0:pr0 t2 t3 ⇒
the thesis becomes ∀i:nat.∀u:T.∀c2:C.∀t0:T.∀H1:(fsubst0 i u c t3 c2 t0).∀e:C.(getl i c (CHead e (Bind Abbr) u))→(pc3 c2 t2 t0)
assume i: nat
assume u: T
assume c2: C
assume t0: T
suppose H1: fsubst0 i u c t3 c2 t0
we proceed by induction on H1 to prove ∀e:C.(getl i c (CHead e (Bind Abbr) u))→(pc3 c2 t2 t0)
case fsubst0_snd : t4:T H2:subst0 i u t3 t4 ⇒
the thesis becomes ∀e:C.∀H3:(getl i c (CHead e (Bind Abbr) u)).(pc3 c t2 t4)
assume e: C
suppose H3: getl i c (CHead e (Bind Abbr) u)
(h1)
by (pr2_free . . . H0)
pr2 c t2 t3
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t3 t3
by (pr2_delta . . . . H3 . . previous . H2)
we proved pr2 c t3 t4
by (pc3_pr2_r . . . previous)
pc3 c t3 t4
end of h2
by (pc3_pr2_u . . . h1 . h2)
we proved pc3 c t2 t4
∀e:C.∀H3:(getl i c (CHead e (Bind Abbr) u)).(pc3 c t2 t4)
case fsubst0_fst : c0:C :csubst0 i u c c0 ⇒
the thesis becomes ∀e:C.(getl i c (CHead e (Bind Abbr) u))→(pc3 c0 t2 t3)
assume e: C
suppose : getl i c (CHead e (Bind Abbr) u)
by (pr2_free . . . H0)
we proved pr2 c0 t2 t3
by (pc3_pr2_r . . . previous)
we proved pc3 c0 t2 t3
∀e:C.(getl i c (CHead e (Bind Abbr) u))→(pc3 c0 t2 t3)
case fsubst0_both : t4:T H2:subst0 i u t3 t4 c0:C H3:csubst0 i u c c0 ⇒
the thesis becomes ∀e:C.∀H4:(getl i c (CHead e (Bind Abbr) u)).(pc3 c0 t2 t4)
assume e: C
suppose H4: getl i c (CHead e (Bind Abbr) u)
(h1) by (pr2_free . . . H0) we proved pr2 c0 t2 t3
(h2)
(h1)
by (le_n .)
we proved le i i
by (csubst0_getl_ge . . previous . . . H3 . H4)
getl i c0 (CHead e (Bind Abbr) u)
end of h1
(h2) by (pr0_refl .) we proved pr0 t3 t3
by (pr2_delta . . . . h1 . . h2 . H2)
we proved pr2 c0 t3 t4
by (pc3_pr2_r . . . previous)
pc3 c0 t3 t4
end of h2
by (pc3_pr2_u . . . h1 . h2)
we proved pc3 c0 t2 t4
∀e:C.∀H4:(getl i c (CHead e (Bind Abbr) u)).(pc3 c0 t2 t4)
we proved ∀e:C.(getl i c (CHead e (Bind Abbr) u))→(pc3 c2 t2 t0)
∀i:nat.∀u:T.∀c2:C.∀t0:T.∀H1:(fsubst0 i u c t3 c2 t0).∀e:C.(getl i c (CHead e (Bind Abbr) u))→(pc3 c2 t2 t0)
case pr2_delta : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abbr) u) t2:T t3:T H1:pr0 t2 t3 t0:T H2:subst0 i u t3 t0 ⇒
the thesis becomes ∀i0:nat.∀u0:T.∀c2:C.∀t4:T.∀H3:(fsubst0 i0 u0 c t0 c2 t4).∀e:C.(getl i0 c (CHead e (Bind Abbr) u0))→(pc3 c2 t2 t4)
assume i0: nat
assume u0: T
assume c2: C
assume t4: T
suppose H3: fsubst0 i0 u0 c t0 c2 t4
we proceed by induction on H3 to prove ∀e:C.(getl i0 c (CHead e (Bind Abbr) u0))→(pc3 c2 t2 t4)
case fsubst0_snd : t5:T H4:subst0 i0 u0 t0 t5 ⇒
the thesis becomes ∀e:C.∀H5:(getl i0 c (CHead e (Bind Abbr) u0)).(pc3 c t2 t5)
assume e: C
suppose H5: getl i0 c (CHead e (Bind Abbr) u0)
(h1)
by (pr2_free . . . H1)
we proved pr2 c t2 t3
by (pr3_pr2 . . . previous)
we proved pr3 c t2 t3
by (pc3_pr3_r . . . previous)
pc3 c t2 t3
end of h1
(h2)
(h1)
by (pr0_refl .)
we proved pr0 t3 t3
by (pr2_delta . . . . H0 . . previous . H2)
pr2 c t3 t0
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t0 t0
by (pr2_delta . . . . H5 . . previous . H4)
we proved pr2 c t0 t5
by (pr3_pr2 . . . previous)
pr3 c t0 t5
end of h2
by (pr3_sing . . . h1 . h2)
we proved pr3 c t3 t5
by (pc3_pr3_r . . . previous)
pc3 c t3 t5
end of h2
by (pc3_t . . . h1 . h2)
we proved pc3 c t2 t5
∀e:C.∀H5:(getl i0 c (CHead e (Bind Abbr) u0)).(pc3 c t2 t5)
case fsubst0_fst : c0:C H4:csubst0 i0 u0 c c0 ⇒
the thesis becomes ∀e:C.∀H5:(getl i0 c (CHead e (Bind Abbr) u0)).(pc3 c0 t2 t0)
assume e: C
suppose H5: getl i0 c (CHead e (Bind Abbr) u0)
(h1)
suppose H6: lt i i0
(H7)
by (csubst0_getl_lt . . H6 . . . H4 . H0)
or4
getl i c0 (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 i c0 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i0 (S i)) 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 i c0 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i0 (S i)) 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 i c0 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i0 (S i)) u0 u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2
end of H7
we proceed by induction on H7 to prove pc3 c0 t2 t0
case or4_intro0 : H8:getl i c0 (CHead d (Bind Abbr) u) ⇒
the thesis becomes pc3 c0 t2 t0
by (pr2_delta . . . . H8 . . H1 . H2)
we proved pr2 c0 t2 t0
by (pc3_pr2_r . . . previous)
pc3 c0 t2 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 i c0 (CHead e0 (Bind b) w) λ:B.λ:C.λu1:T.λw:T.subst0 (minus i0 (S i)) u0 u1 w ⇒
the thesis becomes pc3 c0 t2 t0
we proceed by induction on H8 to prove pc3 c0 t2 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 i c0 (CHead x1 (Bind x0) x3) H11:subst0 (minus i0 (S i)) u0 x2 x3 ⇒
the thesis becomes pc3 c0 t2 t0
(H12)
by (f_equal . . . . . H9)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c3 ⇒c3
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (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 t5⇒t5
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t5⇒t5
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t5⇒t5 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t5⇒t5 (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 t5⇒t5
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t5⇒t5
that is equivalent to eq T u x2
by (eq_ind_r . . . H11 . previous)
subst0 (minus i0 (S i)) u0 u x3
end of H17
(H18)
by (eq_ind_r . . . H10 . H16)
getl i c0 (CHead d (Bind x0) x3)
end of H18
(H19)
by (eq_ind_r . . . H18 . H15)
getl i c0 (CHead d (Bind Abbr) x3)
end of H19
by (subst0_subst0_back . . . . H2 . . . H17)
we proved ex2 T λt:T.subst0 i x3 t3 t λt:T.subst0 (S (plus (minus i0 (S i)) i)) u0 t0 t
we proceed by induction on the previous result to prove pc3 c0 t2 t0
case ex_intro2 : x:T H20:subst0 i x3 t3 x H21:subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x ⇒
the thesis becomes pc3 c0 t2 t0
(H22)
by (lt_plus_minus_r . . H6)
we proved eq nat i0 (S (plus (minus i0 (S i)) i))
by (eq_ind_r . . . H21 . previous)
subst0 i0 u0 t0 x
end of H22
(h1)
by (pr2_delta . . . . H19 . . H1 . H20)
pr2 c0 t2 x
end of h1
(h2)
(h1)
by (le_n .)
we proved le i0 i0
by (csubst0_getl_ge . . previous . . . H4 . H5)
getl i0 c0 (CHead e (Bind Abbr) u0)
end of h1
(h2) by (pr0_refl .) we proved pr0 t0 t0
by (pr2_delta . . . . h1 . . h2 . H22)
we proved pr2 c0 t0 x
by (pc3_pr2_x . . . previous)
pc3 c0 x t0
end of h2
by (pc3_pr2_u . . . h1 . h2)
pc3 c0 t2 t0
we proved pc3 c0 t2 t0
(eq B Abbr x0)→(eq C d x1)→(pc3 c0 t2 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)→(pc3 c0 t2 t0)
end of h1
(h2)
consider H12
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c3 ⇒c3
eq C d x1
end of h2
by (h1 h2)
pc3 c0 t2 t0
pc3 c0 t2 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 i c0 (CHead e2 (Bind b) u1) λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2 ⇒
the thesis becomes pc3 c0 t2 t0
we proceed by induction on H8 to prove pc3 c0 t2 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 i c0 (CHead x2 (Bind x0) x3) H11:csubst0 (minus i0 (S i)) u0 x1 x2 ⇒
the thesis becomes pc3 c0 t2 t0
(H12)
by (f_equal . . . . . H9)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c3 ⇒c3
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (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 t5⇒t5
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t5⇒t5
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t5⇒t5 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t5⇒t5 (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 t5⇒t5
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t5⇒t5
that is equivalent to eq T u x3
by (eq_ind_r . . . H10 . previous)
getl i c0 (CHead x2 (Bind x0) u)
end of H17
(H19)
by (eq_ind_r . . . H17 . H15)
getl i c0 (CHead x2 (Bind Abbr) u)
end of H19
by (pr2_delta . . . . H19 . . H1 . H2)
we proved pr2 c0 t2 t0
by (pc3_pr2_r . . . previous)
we proved pc3 c0 t2 t0
(eq B Abbr x0)→(eq C d x1)→(pc3 c0 t2 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)→(pc3 c0 t2 t0)
end of h1
(h2)
consider H12
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c3 ⇒c3
eq C d x1
end of h2
by (h1 h2)
pc3 c0 t2 t0
pc3 c0 t2 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 i c0 (CHead e2 (Bind b) w) λ:B.λ:C.λ:C.λu1:T.λw:T.subst0 (minus i0 (S i)) u0 u1 w λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2 ⇒
the thesis becomes pc3 c0 t2 t0
we proceed by induction on H8 to prove pc3 c0 t2 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 i c0 (CHead x2 (Bind x0) x4) H11:subst0 (minus i0 (S i)) u0 x3 x4 H12:csubst0 (minus i0 (S i)) u0 x1 x2 ⇒
the thesis becomes pc3 c0 t2 t0
(H13)
by (f_equal . . . . . H9)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c3 ⇒c3
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (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 t5⇒t5
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t5⇒t5
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t5⇒t5 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t5⇒t5 (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 t5⇒t5
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t5⇒t5
that is equivalent to eq T u x3
by (eq_ind_r . . . H11 . previous)
subst0 (minus i0 (S i)) u0 u x4
end of H18
(H20)
by (eq_ind_r . . . H10 . H16)
getl i c0 (CHead x2 (Bind Abbr) x4)
end of H20
by (subst0_subst0_back . . . . H2 . . . H18)
we proved ex2 T λt:T.subst0 i x4 t3 t λt:T.subst0 (S (plus (minus i0 (S i)) i)) u0 t0 t
we proceed by induction on the previous result to prove pc3 c0 t2 t0
case ex_intro2 : x:T H21:subst0 i x4 t3 x H22:subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x ⇒
the thesis becomes pc3 c0 t2 t0
(H23)
by (lt_plus_minus_r . . H6)
we proved eq nat i0 (S (plus (minus i0 (S i)) i))
by (eq_ind_r . . . H22 . previous)
subst0 i0 u0 t0 x
end of H23
(h1)
by (pr2_delta . . . . H20 . . H1 . H21)
pr2 c0 t2 x
end of h1
(h2)
(h1)
by (le_n .)
we proved le i0 i0
by (csubst0_getl_ge . . previous . . . H4 . H5)
getl i0 c0 (CHead e (Bind Abbr) u0)
end of h1
(h2) by (pr0_refl .) we proved pr0 t0 t0
by (pr2_delta . . . . h1 . . h2 . H23)
we proved pr2 c0 t0 x
by (pc3_pr2_x . . . previous)
pc3 c0 x t0
end of h2
by (pc3_pr2_u . . . h1 . h2)
pc3 c0 t2 t0
we proved pc3 c0 t2 t0
(eq B Abbr x0)→(eq C d x1)→(pc3 c0 t2 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)→(pc3 c0 t2 t0)
end of h1
(h2)
consider H13
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c3 ⇒c3
eq C d x1
end of h2
by (h1 h2)
pc3 c0 t2 t0
pc3 c0 t2 t0
we proved pc3 c0 t2 t0
(lt i i0)→(pc3 c0 t2 t0)
end of h1
(h2)
suppose H6: le i0 i
by (csubst0_getl_ge . . H6 . . . H4 . H0)
we proved getl i c0 (CHead d (Bind Abbr) u)
by (pr2_delta . . . . previous . . H1 . H2)
we proved pr2 c0 t2 t0
by (pc3_pr2_r . . . previous)
we proved pc3 c0 t2 t0
(le i0 i)→(pc3 c0 t2 t0)
end of h2
by (lt_le_e . . . h1 h2)
we proved pc3 c0 t2 t0
∀e:C.∀H5:(getl i0 c (CHead e (Bind Abbr) u0)).(pc3 c0 t2 t0)
case fsubst0_both : t5:T H4:subst0 i0 u0 t0 t5 c0:C H5:csubst0 i0 u0 c c0 ⇒
the thesis becomes ∀e:C.∀H6:(getl i0 c (CHead e (Bind Abbr) u0)).(pc3 c0 t2 t5)
assume e: C
suppose H6: getl i0 c (CHead e (Bind Abbr) u0)
(h1)
suppose H7: lt i i0
(H8)
by (csubst0_getl_lt . . H7 . . . H5 . H0)
or4
getl i c0 (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 i c0 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i0 (S i)) 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 i c0 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i0 (S i)) 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 i c0 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i0 (S i)) u0 u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2
end of H8
we proceed by induction on H8 to prove pc3 c0 t2 t5
case or4_intro0 : H9:getl i c0 (CHead d (Bind Abbr) u) ⇒
the thesis becomes pc3 c0 t2 t5
(h1) by (pr2_free . . . H1) we proved pr2 c0 t2 t3
(h2)
(h1)
by (pr0_refl .)
we proved pr0 t3 t3
by (pr2_delta . . . . H9 . . previous . H2)
pr2 c0 t3 t0
end of h1
(h2)
(h1)
by (le_n .)
we proved le i0 i0
by (csubst0_getl_ge . . previous . . . H5 . H6)
getl i0 c0 (CHead e (Bind Abbr) u0)
end of h1
(h2) by (pr0_refl .) we proved pr0 t0 t0
by (pr2_delta . . . . h1 . . h2 . H4)
we proved pr2 c0 t0 t5
by (pr3_pr2 . . . previous)
pr3 c0 t0 t5
end of h2
by (pr3_sing . . . h1 . h2)
we proved pr3 c0 t3 t5
by (pc3_pr3_r . . . previous)
pc3 c0 t3 t5
end of h2
by (pc3_pr2_u . . . h1 . h2)
pc3 c0 t2 t5
case or4_intro1 : H9: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 i c0 (CHead e0 (Bind b) w) λ:B.λ:C.λu1:T.λw:T.subst0 (minus i0 (S i)) u0 u1 w ⇒
the thesis becomes pc3 c0 t2 t5
we proceed by induction on H9 to prove pc3 c0 t2 t5
case ex3_4_intro : x0:B x1:C x2:T x3:T H10:eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H11:getl i c0 (CHead x1 (Bind x0) x3) H12:subst0 (minus i0 (S i)) u0 x2 x3 ⇒
the thesis becomes pc3 c0 t2 t5
(H13)
by (f_equal . . . . . H10)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c3 ⇒c3
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (CHead x1 (Bind x0) x2)
end of H13
(h1)
(H14)
by (f_equal . . . . . H10)
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 H14
(h1)
(H15)
by (f_equal . . . . . H10)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t6⇒t6
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t6⇒t6
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t6⇒t6 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t6⇒t6 (CHead x1 (Bind x0) x2)
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 t6⇒t6
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t6⇒t6
that is equivalent to eq T u x2
by (eq_ind_r . . . H12 . previous)
subst0 (minus i0 (S i)) u0 u x3
end of H18
(H19)
by (eq_ind_r . . . H11 . H17)
getl i c0 (CHead d (Bind x0) x3)
end of H19
(H20)
by (eq_ind_r . . . H19 . H16)
getl i c0 (CHead d (Bind Abbr) x3)
end of H20
by (subst0_subst0_back . . . . H2 . . . H18)
we proved ex2 T λt:T.subst0 i x3 t3 t λt:T.subst0 (S (plus (minus i0 (S i)) i)) u0 t0 t
we proceed by induction on the previous result to prove pc3 c0 t2 t5
case ex_intro2 : x:T H21:subst0 i x3 t3 x H22:subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x ⇒
the thesis becomes pc3 c0 t2 t5
(H23)
by (lt_plus_minus_r . . H7)
we proved eq nat i0 (S (plus (minus i0 (S i)) i))
by (eq_ind_r . . . H22 . previous)
subst0 i0 u0 t0 x
end of H23
(h1)
by (pr2_delta . . . . H20 . . H1 . H21)
pr2 c0 t2 x
end of h1
(h2)
(h1)
(h1)
by (le_n .)
we proved le i0 i0
by (csubst0_getl_ge . . previous . . . H5 . H6)
getl i0 c0 (CHead e (Bind Abbr) u0)
end of h1
(h2) by (pr0_refl .) we proved pr0 t0 t0
by (pr2_delta . . . . h1 . . h2 . H23)
pr2 c0 t0 x
end of h1
(h2)
(h1)
by (le_n .)
we proved le i0 i0
by (csubst0_getl_ge . . previous . . . H5 . H6)
getl i0 c0 (CHead e (Bind Abbr) u0)
end of h1
(h2) by (pr0_refl .) we proved pr0 t0 t0
by (pr2_delta . . . . h1 . . h2 . H4)
we proved pr2 c0 t0 t5
by (pc3_pr2_r . . . previous)
pc3 c0 t0 t5
end of h2
by (pc3_pr2_u2 . . . h1 . h2)
pc3 c0 x t5
end of h2
by (pc3_pr2_u . . . h1 . h2)
pc3 c0 t2 t5
we proved pc3 c0 t2 t5
(eq B Abbr x0)→(eq C d x1)→(pc3 c0 t2 t5)
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) 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)→(pc3 c0 t2 t5)
end of h1
(h2)
consider H13
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c3 ⇒c3
eq C d x1
end of h2
by (h1 h2)
pc3 c0 t2 t5
pc3 c0 t2 t5
case or4_intro2 : H9: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 i c0 (CHead e2 (Bind b) u1) λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2 ⇒
the thesis becomes pc3 c0 t2 t5
we proceed by induction on H9 to prove pc3 c0 t2 t5
case ex3_4_intro : x0:B x1:C x2:C x3:T H10:eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H11:getl i c0 (CHead x2 (Bind x0) x3) H12:csubst0 (minus i0 (S i)) u0 x1 x2 ⇒
the thesis becomes pc3 c0 t2 t5
(H13)
by (f_equal . . . . . H10)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c3 ⇒c3
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (CHead x1 (Bind x0) x3)
end of H13
(h1)
(H14)
by (f_equal . . . . . H10)
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 . . . . . H10)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t6⇒t6
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t6⇒t6
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t6⇒t6 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t6⇒t6 (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 t6⇒t6
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t6⇒t6
that is equivalent to eq T u x3
by (eq_ind_r . . . H11 . previous)
getl i c0 (CHead x2 (Bind x0) u)
end of H18
(H20)
by (eq_ind_r . . . H18 . H16)
getl i c0 (CHead x2 (Bind Abbr) u)
end of H20
(h1)
by (pr2_delta . . . . H20 . . H1 . H2)
pr2 c0 t2 t0
end of h1
(h2)
(h1)
by (le_n .)
we proved le i0 i0
by (csubst0_getl_ge . . previous . . . H5 . H6)
getl i0 c0 (CHead e (Bind Abbr) u0)
end of h1
(h2) by (pr0_refl .) we proved pr0 t0 t0
by (pr2_delta . . . . h1 . . h2 . H4)
we proved pr2 c0 t0 t5
by (pc3_pr2_r . . . previous)
pc3 c0 t0 t5
end of h2
by (pc3_pr2_u . . . h1 . h2)
we proved pc3 c0 t2 t5
(eq B Abbr x0)→(eq C d x1)→(pc3 c0 t2 t5)
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)→(pc3 c0 t2 t5)
end of h1
(h2)
consider H13
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c3 ⇒c3
eq C d x1
end of h2
by (h1 h2)
pc3 c0 t2 t5
pc3 c0 t2 t5
case or4_intro3 : H9: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 i c0 (CHead e2 (Bind b) w) λ:B.λ:C.λ:C.λu1:T.λw:T.subst0 (minus i0 (S i)) u0 u1 w λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i0 (S i)) u0 e1 e2 ⇒
the thesis becomes pc3 c0 t2 t5
we proceed by induction on H9 to prove pc3 c0 t2 t5
case ex4_5_intro : x0:B x1:C x2:C x3:T x4:T H10:eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H11:getl i c0 (CHead x2 (Bind x0) x4) H12:subst0 (minus i0 (S i)) u0 x3 x4 H13:csubst0 (minus i0 (S i)) u0 x1 x2 ⇒
the thesis becomes pc3 c0 t2 t5
(H14)
by (f_equal . . . . . H10)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c3 ⇒c3
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c3 ⇒c3 (CHead x1 (Bind x0) x3)
end of H14
(h1)
(H15)
by (f_equal . . . . . H10)
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 H15
(h1)
(H16)
by (f_equal . . . . . H10)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t6⇒t6
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t6⇒t6
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t6⇒t6 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t6⇒t6 (CHead x1 (Bind x0) x3)
end of H16
suppose H17: eq B Abbr x0
suppose H18: eq C d x1
(H19)
consider H16
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t6⇒t6
<λ:C.T> CASE CHead x1 (Bind x0) x3 OF CSort ⇒u | CHead t6⇒t6
that is equivalent to eq T u x3
by (eq_ind_r . . . H12 . previous)
subst0 (minus i0 (S i)) u0 u x4
end of H19
(H21)
by (eq_ind_r . . . H11 . H17)
getl i c0 (CHead x2 (Bind Abbr) x4)
end of H21
by (subst0_subst0_back . . . . H2 . . . H19)
we proved ex2 T λt:T.subst0 i x4 t3 t λt:T.subst0 (S (plus (minus i0 (S i)) i)) u0 t0 t
we proceed by induction on the previous result to prove pc3 c0 t2 t5
case ex_intro2 : x:T H22:subst0 i x4 t3 x H23:subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x ⇒
the thesis becomes pc3 c0 t2 t5
(H24)
by (lt_plus_minus_r . . H7)
we proved eq nat i0 (S (plus (minus i0 (S i)) i))
by (eq_ind_r . . . H23 . previous)
subst0 i0 u0 t0 x
end of H24
(h1)
by (pr2_delta . . . . H21 . . H1 . H22)
pr2 c0 t2 x
end of h1
(h2)
(h1)
(h1)
by (le_n .)
we proved le i0 i0
by (csubst0_getl_ge . . previous . . . H5 . H6)
getl i0 c0 (CHead e (Bind Abbr) u0)
end of h1
(h2) by (pr0_refl .) we proved pr0 t0 t0
by (pr2_delta . . . . h1 . . h2 . H24)
pr2 c0 t0 x
end of h1
(h2)
(h1)
by (le_n .)
we proved le i0 i0
by (csubst0_getl_ge . . previous . . . H5 . H6)
getl i0 c0 (CHead e (Bind Abbr) u0)
end of h1
(h2) by (pr0_refl .) we proved pr0 t0 t0
by (pr2_delta . . . . h1 . . h2 . H4)
we proved pr2 c0 t0 t5
by (pc3_pr2_r . . . previous)
pc3 c0 t0 t5
end of h2
by (pc3_pr2_u2 . . . h1 . h2)
pc3 c0 x t5
end of h2
by (pc3_pr2_u . . . h1 . h2)
pc3 c0 t2 t5
we proved pc3 c0 t2 t5
(eq B Abbr x0)→(eq C d x1)→(pc3 c0 t2 t5)
end of h1
(h2)
consider H15
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)→(pc3 c0 t2 t5)
end of h1
(h2)
consider H14
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c3 ⇒c3
<λ:C.C> CASE CHead x1 (Bind x0) x3 OF CSort ⇒d | CHead c3 ⇒c3
eq C d x1
end of h2
by (h1 h2)
pc3 c0 t2 t5
pc3 c0 t2 t5
we proved pc3 c0 t2 t5
(lt i i0)→(pc3 c0 t2 t5)
end of h1
(h2)
suppose H7: le i0 i
(h1)
by (csubst0_getl_ge . . H7 . . . H5 . H0)
we proved getl i c0 (CHead d (Bind Abbr) u)
by (pr2_delta . . . . previous . . H1 . H2)
pr2 c0 t2 t0
end of h1
(h2)
(h1)
by (le_n .)
we proved le i0 i0
by (csubst0_getl_ge . . previous . . . H5 . H6)
getl i0 c0 (CHead e (Bind Abbr) u0)
end of h1
(h2) by (pr0_refl .) we proved pr0 t0 t0
by (pr2_delta . . . . h1 . . h2 . H4)
we proved pr2 c0 t0 t5
by (pc3_pr2_r . . . previous)
pc3 c0 t0 t5
end of h2
by (pc3_pr2_u . . . h1 . h2)
we proved pc3 c0 t2 t5
(le i0 i)→(pc3 c0 t2 t5)
end of h2
by (lt_le_e . . . h1 h2)
we proved pc3 c0 t2 t5
∀e:C.∀H6:(getl i0 c (CHead e (Bind Abbr) u0)).(pc3 c0 t2 t5)
we proved ∀e:C.(getl i0 c (CHead e (Bind Abbr) u0))→(pc3 c2 t2 t4)
∀i0:nat.∀u0:T.∀c2:C.∀t4:T.∀H3:(fsubst0 i0 u0 c t0 c2 t4).∀e:C.(getl i0 c (CHead e (Bind Abbr) u0))→(pc3 c2 t2 t4)
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))→(pc3 c2 t t3)
we proved
∀c1:C
.∀t:T
.∀t1:T
.pr2 c1 t t1
→∀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))→(pc3 c2 t t3)