DEFINITION csubt_getl_abst()
TYPE =
∀g:G
.∀c1:C
.∀d1:C
.∀t:T
.∀n:nat
.getl n c1 (CHead d1 (Bind Abst) t)
→∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
BODY =
assume g: G
assume c1: C
assume d1: C
assume t: T
assume n: nat
suppose H: getl n c1 (CHead d1 (Bind Abst) t)
(H0)
by (getl_gen_all . . . H)
ex2 C λe:C.drop n O c1 e λe:C.clear e (CHead d1 (Bind Abst) t)
end of H0
we proceed by induction on H0 to prove
∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
case ex_intro2 : x:C H1:drop n O c1 x H2:clear x (CHead d1 (Bind Abst) t) ⇒
the thesis becomes
∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
assume n0: nat
suppose : drop n O c1 (CSort n0)
suppose H4: clear (CSort n0) (CHead d1 (Bind Abst) t)
by (clear_gen_sort . . H4 .)
we proved
∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
drop n O c1 (CSort n0)
→∀H4:clear (CSort n0) (CHead d1 (Bind Abst) t)
.∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
assume x0: C
suppose :
drop n O c1 x0
→(clear x0 (CHead d1 (Bind Abst) t)
→∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t))
assume k: K
assume t0: T
suppose H3: drop n O c1 (CHead x0 k t0)
suppose H4: clear (CHead x0 k t0) (CHead d1 (Bind Abst) t)
assume b: B
suppose H5: drop n O c1 (CHead x0 (Bind b) t0)
suppose H6: clear (CHead x0 (Bind b) t0) (CHead d1 (Bind Abst) t)
(H7)
by (clear_gen_bind . . . . H6)
we proved eq C (CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Abst) t OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead x0 (Bind b) t0 OF CSort ⇒d1 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead d1 (Bind Abst) t)
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead x0 (Bind b) t0)
end of H7
(h1)
(H8)
by (clear_gen_bind . . . . H6)
we proved eq C (CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind Abst) t OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
<λ:C.B>
CASE CHead x0 (Bind b) t0 OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
CHead d1 (Bind Abst) t
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
CHead x0 (Bind b) t0
end of H8
(h1)
(H9)
by (clear_gen_bind . . . . H6)
we proved eq C (CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d1 (Bind Abst) t OF CSort ⇒t | CHead t1⇒t1
<λ:C.T> CASE CHead x0 (Bind b) t0 OF CSort ⇒t | CHead t1⇒t1
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒t | CHead t1⇒t1 (CHead d1 (Bind Abst) t)
λe:C.<λ:C.T> CASE e OF CSort ⇒t | CHead t1⇒t1 (CHead x0 (Bind b) t0)
end of H9
suppose H10: eq B Abst b
suppose H11: eq C d1 x0
assume c2: C
suppose H12: csubt g c1 c2
(H13)
consider H9
we proved
eq
T
<λ:C.T> CASE CHead d1 (Bind Abst) t OF CSort ⇒t | CHead t1⇒t1
<λ:C.T> CASE CHead x0 (Bind b) t0 OF CSort ⇒t | CHead t1⇒t1
that is equivalent to eq T t t0
by (eq_ind_r . . . H5 . previous)
drop n O c1 (CHead x0 (Bind b) t)
end of H13
(H14)
by (eq_ind_r . . . H13 . H10)
drop n O c1 (CHead x0 (Bind Abst) t)
end of H14
(H15)
by (eq_ind_r . . . H14 . H11)
drop n O c1 (CHead d1 (Bind Abst) t)
end of H15
by (csubt_drop_abst . . . . H12 . . H15)
we proved
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop n O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on the previous result to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case or_introl : H16:ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Bind Abst) t) ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on H16 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex_intro2 : x1:C H17:csubt g d1 x1 H18:drop n O c2 (CHead x1 (Bind Abst) t) ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (clear_bind . . .)
we proved clear (CHead x1 (Bind Abst) t) (CHead x1 (Bind Abst) t)
by (getl_intro . . . . H18 previous)
we proved getl n c2 (CHead x1 (Bind Abst) t)
by (ex_intro2 . . . . H17 previous)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
by (or_introl . . previous)
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case or_intror : H16:ex4_2 C T λd2:C.λ:T.csubt g d1 d2 λd2:C.λu:T.drop n O c2 (CHead d2 (Bind Abbr) u) λ:C.λu:T.ty3 g d1 u t λd2:C.λu:T.ty3 g d2 u t ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on H16 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex4_2_intro : x1:C x2:T H17:csubt g d1 x1 H18:drop n O c2 (CHead x1 (Bind Abbr) x2) H19:ty3 g d1 x2 t H20:ty3 g x1 x2 t ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (clear_bind . . .)
we proved clear (CHead x1 (Bind Abbr) x2) (CHead x1 (Bind Abbr) x2)
by (getl_intro . . . . H18 previous)
we proved getl n c2 (CHead x1 (Bind Abbr) x2)
by (ex4_2_intro . . . . . . . . H17 previous H19 H20)
we proved
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (or_intror . . previous)
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proved
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
eq B Abst b
→(eq C d1 x0
→∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t))
end of h1
(h2)
consider H8
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind Abst) t OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
<λ:C.B>
CASE CHead x0 (Bind b) t0 OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
eq B Abst b
end of h2
by (h1 h2)
eq C d1 x0
→∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
end of h1
(h2)
consider H7
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Abst) t OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead x0 (Bind b) t0 OF CSort ⇒d1 | CHead c ⇒c
eq C d1 x0
end of h2
by (h1 h2)
we proved
∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
∀H5:drop n O c1 (CHead x0 (Bind b) t0)
.∀H6:clear (CHead x0 (Bind b) t0) (CHead d1 (Bind Abst) t)
.∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
assume f: F
suppose H5: drop n O c1 (CHead x0 (Flat f) t0)
suppose H6: clear (CHead x0 (Flat f) t0) (CHead d1 (Bind Abst) t)
(H7) consider H5
we proceed by induction on n to prove
∀x1:C
.drop n O x1 (CHead x0 (Flat f) t0)
→∀c2:C
.csubt g x1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
case O : ⇒
the thesis becomes
∀x1:C
.drop O O x1 (CHead x0 (Flat f) t0)
→∀c2:C
.csubt g x1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
assume x1: C
suppose H8: drop O O x1 (CHead x0 (Flat f) t0)
assume c2: C
suppose H9: csubt g x1 c2
(H10)
by (drop_gen_refl . . H8)
we proved eq C x1 (CHead x0 (Flat f) t0)
we proceed by induction on the previous result to prove csubt g (CHead x0 (Flat f) t0) c2
case refl_equal : ⇒
the thesis becomes the hypothesis H9
csubt g (CHead x0 (Flat f) t0) c2
end of H10
(H_y)
by (clear_gen_flat . . . . H6)
we proved clear x0 (CHead d1 (Bind Abst) t)
by (clear_flat . . previous . .)
clear (CHead x0 (Flat f) t0) (CHead d1 (Bind Abst) t)
end of H_y
(H11)
by (csubt_clear_conf . . . H10 . H_y)
ex2 C λe2:C.csubt g (CHead d1 (Bind Abst) t) e2 λe2:C.clear c2 e2
end of H11
we proceed by induction on H11 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex_intro2 : x2:C H12:csubt g (CHead d1 (Bind Abst) t) x2 H13:clear c2 x2 ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
(H14)
by (csubt_gen_abst . . . . H12)
or
ex2 C λe2:C.eq C x2 (CHead e2 (Bind Abst) t) λe2:C.csubt g d1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C x2 (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g d1 e2
λ:C.λv2:T.ty3 g d1 v2 t
λe2:C.λv2:T.ty3 g e2 v2 t
end of H14
we proceed by induction on H14 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case or_introl : H15:ex2 C λe2:C.eq C x2 (CHead e2 (Bind Abst) t) λe2:C.csubt g d1 e2 ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on H15 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex_intro2 : x3:C H16:eq C x2 (CHead x3 (Bind Abst) t) H17:csubt g d1 x3 ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
(H18)
we proceed by induction on H16 to prove clear c2 (CHead x3 (Bind Abst) t)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
clear c2 (CHead x3 (Bind Abst) t)
end of H18
by (drop_refl .)
we proved drop O O c2 c2
by (getl_intro . . . . previous H18)
we proved getl O c2 (CHead x3 (Bind Abst) t)
by (ex_intro2 . . . . H17 previous)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
by (or_introl . . previous)
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case or_intror : H15:ex4_2 C T λe2:C.λv2:T.eq C x2 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g d1 e2 λ:C.λv2:T.ty3 g d1 v2 t λe2:C.λv2:T.ty3 g e2 v2 t ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on H15 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex4_2_intro : x3:C x4:T H16:eq C x2 (CHead x3 (Bind Abbr) x4) H17:csubt g d1 x3 H18:ty3 g d1 x4 t H19:ty3 g x3 x4 t ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
(H20)
we proceed by induction on H16 to prove clear c2 (CHead x3 (Bind Abbr) x4)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
clear c2 (CHead x3 (Bind Abbr) x4)
end of H20
by (drop_refl .)
we proved drop O O c2 c2
by (getl_intro . . . . previous H20)
we proved getl O c2 (CHead x3 (Bind Abbr) x4)
by (ex4_2_intro . . . . . . . . H17 previous H18 H19)
we proved
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (or_intror . . previous)
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proved
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
∀x1:C
.drop O O x1 (CHead x0 (Flat f) t0)
→∀c2:C
.csubt g x1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
case S : n0:nat ⇒
the thesis becomes
∀x1:C
.∀H9:drop (S n0) O x1 (CHead x0 (Flat f) t0)
.∀c2:C
.∀H10:csubt g x1 c2
.or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
(H8) by induction hypothesis we know
∀x1:C
.drop n0 O x1 (CHead x0 (Flat f) t0)
→∀c2:C
.csubt g x1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n0 c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n0 c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
assume x1: C
suppose H9: drop (S n0) O x1 (CHead x0 (Flat f) t0)
assume c2: C
suppose H10: csubt g x1 c2
(H11)
by (drop_clear . . . H9)
ex2_3
B
C
T
λb:B.λe:C.λv:T.clear x1 (CHead e (Bind b) v)
λ:B.λe:C.λ:T.drop n0 O e (CHead x0 (Flat f) t0)
end of H11
we proceed by induction on H11 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex2_3_intro : x2:B x3:C x4:T H12:clear x1 (CHead x3 (Bind x2) x4) H13:drop n0 O x3 (CHead x0 (Flat f) t0) ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
(H14)
by (csubt_clear_conf . . . H10 . H12)
ex2 C λe2:C.csubt g (CHead x3 (Bind x2) x4) e2 λe2:C.clear c2 e2
end of H14
we proceed by induction on H14 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex_intro2 : x5:C H15:csubt g (CHead x3 (Bind x2) x4) x5 H16:clear c2 x5 ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
(H17)
by (csubt_gen_bind . . . . . H15)
ex2_3 B C T λb2:B.λe2:C.λv2:T.eq C x5 (CHead e2 (Bind b2) v2) λ:B.λe2:C.λ:T.csubt g x3 e2
end of H17
we proceed by induction on H17 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex2_3_intro : x6:B x7:C x8:T H18:eq C x5 (CHead x7 (Bind x6) x8) H19:csubt g x3 x7 ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
(H20)
we proceed by induction on H18 to prove clear c2 (CHead x7 (Bind x6) x8)
case refl_equal : ⇒
the thesis becomes the hypothesis H16
clear c2 (CHead x7 (Bind x6) x8)
end of H20
(H21)
by (H8 . H13 . H19)
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n0 x7 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n0 x7 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
end of H21
we proceed by induction on H21 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case or_introl : H22:ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n0 x7 (CHead d2 (Bind Abst) t) ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on H22 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex_intro2 : x9:C H23:csubt g d1 x9 H24:getl n0 x7 (CHead x9 (Bind Abst) t) ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (getl_clear_bind . . . . H20 . . H24)
we proved getl (S n0) c2 (CHead x9 (Bind Abst) t)
by (ex_intro2 . . . . H23 previous)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
by (or_introl . . previous)
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case or_intror : H22:ex4_2 C T λd2:C.λ:T.csubt g d1 d2 λd2:C.λu:T.getl n0 x7 (CHead d2 (Bind Abbr) u) λ:C.λu:T.ty3 g d1 u t λd2:C.λu:T.ty3 g d2 u t ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on H22 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex4_2_intro : x9:C x10:T H23:csubt g d1 x9 H24:getl n0 x7 (CHead x9 (Bind Abbr) x10) H25:ty3 g d1 x10 t H26:ty3 g x9 x10 t ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (getl_clear_bind . . . . H20 . . H24)
we proved getl (S n0) c2 (CHead x9 (Bind Abbr) x10)
by (ex4_2_intro . . . . . . . . H23 previous H25 H26)
we proved
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (or_intror . . previous)
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proved
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
∀x1:C
.∀H9:drop (S n0) O x1 (CHead x0 (Flat f) t0)
.∀c2:C
.∀H10:csubt g x1 c2
.or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proved
∀x1:C
.drop n O x1 (CHead x0 (Flat f) t0)
→∀c2:C
.csubt g x1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
by (unintro . . . previous H7)
we proved
∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
∀H5:drop n O c1 (CHead x0 (Flat f) t0)
.∀H6:clear (CHead x0 (Flat f) t0) (CHead d1 (Bind Abst) t)
.∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
by (previous . H3 H4)
we proved
∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
∀H3:drop n O c1 (CHead x0 k t0)
.∀H4:clear (CHead x0 k t0) (CHead d1 (Bind Abst) t)
.∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
by (previous . H1 H2)
∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
we proved
∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
we proved
∀g:G
.∀c1:C
.∀d1:C
.∀t:T
.∀n:nat
.getl n c1 (CHead d1 (Bind Abst) t)
→∀c2:C
.csubt g c1 c2
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)