DEFINITION csubt_getl_abbr()
TYPE =
∀g:G
.∀c1:C
.∀d1:C
.∀u:T
.∀n:nat
.getl n c1 (CHead d1 (Bind Abbr) u)
→∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
BODY =
assume g: G
assume c1: C
assume d1: C
assume u: T
assume n: nat
suppose H: getl n c1 (CHead d1 (Bind Abbr) u)
(H0)
by (getl_gen_all . . . H)
ex2 C λe:C.drop n O c1 e λe:C.clear e (CHead d1 (Bind Abbr) u)
end of H0
we proceed by induction on H0 to prove
∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
case ex_intro2 : x:C H1:drop n O c1 x H2:clear x (CHead d1 (Bind Abbr) u) ⇒
the thesis becomes
∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
assume n0: nat
suppose : drop n O c1 (CSort n0)
suppose H4: clear (CSort n0) (CHead d1 (Bind Abbr) u)
by (clear_gen_sort . . H4 .)
we proved
∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
drop n O c1 (CSort n0)
→∀H4:clear (CSort n0) (CHead d1 (Bind Abbr) u)
.∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
assume x0: C
suppose :
drop n O c1 x0
→(clear x0 (CHead d1 (Bind Abbr) u)
→∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u))
assume k: K
assume t: T
suppose H3: drop n O c1 (CHead x0 k t)
suppose H4: clear (CHead x0 k t) (CHead d1 (Bind Abbr) u)
assume b: B
suppose H5: drop n O c1 (CHead x0 (Bind b) t)
suppose H6: clear (CHead x0 (Bind b) t) (CHead d1 (Bind Abbr) u)
(H7)
by (clear_gen_bind . . . . H6)
we proved eq C (CHead d1 (Bind Abbr) u) (CHead x0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Abbr) u OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead x0 (Bind b) t OF CSort ⇒d1 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead d1 (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead x0 (Bind b) t)
end of H7
(h1)
(H8)
by (clear_gen_bind . . . . H6)
we proved eq C (CHead d1 (Bind Abbr) u) (CHead x0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead x0 (Bind b) t OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
CHead d1 (Bind Abbr) u
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
CHead x0 (Bind b) t
end of H8
(h1)
(H9)
by (clear_gen_bind . . . . H6)
we proved eq C (CHead d1 (Bind Abbr) u) (CHead x0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d1 (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind b) t OF CSort ⇒u | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead d1 (Bind Abbr) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead x0 (Bind b) t)
end of H9
suppose H10: eq B Abbr 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 Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind b) t OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u t
by (eq_ind_r . . . H5 . previous)
drop n O c1 (CHead x0 (Bind b) u)
end of H13
(H14)
by (eq_ind_r . . . H13 . H10)
drop n O c1 (CHead x0 (Bind Abbr) u)
end of H14
(H15)
by (eq_ind_r . . . H14 . H11)
drop n O c1 (CHead d1 (Bind Abbr) u)
end of H15
by (csubt_drop_abbr . . . . H12 . . H15)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Bind Abbr) u)
we proceed by induction on the previous result to prove ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
case ex_intro2 : x1:C H16:csubt g d1 x1 H17:drop n O c2 (CHead x1 (Bind Abbr) u) ⇒
the thesis becomes ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
by (clear_bind . . .)
we proved clear (CHead x1 (Bind Abbr) u) (CHead x1 (Bind Abbr) u)
by (getl_intro . . . . H17 previous)
we proved getl n c2 (CHead x1 (Bind Abbr) u)
by (ex_intro2 . . . . H16 previous)
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
eq B Abbr b
→(eq C d1 x0
→∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u))
end of h1
(h2)
consider H8
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead x0 (Bind b) t OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
eq B Abbr b
end of h2
by (h1 h2)
eq C d1 x0
→∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
end of h1
(h2)
consider H7
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Abbr) u OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead x0 (Bind b) t OF CSort ⇒d1 | CHead c ⇒c
eq C d1 x0
end of h2
by (h1 h2)
we proved
∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
∀H5:drop n O c1 (CHead x0 (Bind b) t)
.∀H6:clear (CHead x0 (Bind b) t) (CHead d1 (Bind Abbr) u)
.∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
assume f: F
suppose H5: drop n O c1 (CHead x0 (Flat f) t)
suppose H6: clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abbr) u)
(H7) consider H5
we proceed by induction on n to prove
∀x1:C
.drop n O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csubt g x1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
case O : ⇒
the thesis becomes
∀x1:C
.drop O O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csubt g x1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abbr) u)
assume x1: C
suppose H8: drop O O x1 (CHead x0 (Flat f) t)
assume c2: C
suppose H9: csubt g x1 c2
(H10)
by (drop_gen_refl . . H8)
we proved eq C x1 (CHead x0 (Flat f) t)
we proceed by induction on the previous result to prove csubt g (CHead x0 (Flat f) t) c2
case refl_equal : ⇒
the thesis becomes the hypothesis H9
csubt g (CHead x0 (Flat f) t) c2
end of H10
(H_y)
by (clear_gen_flat . . . . H6)
we proved clear x0 (CHead d1 (Bind Abbr) u)
by (clear_flat . . previous . .)
clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abbr) u)
end of H_y
(H11)
by (csubt_clear_conf . . . H10 . H_y)
ex2 C λe2:C.csubt g (CHead d1 (Bind Abbr) u) e2 λe2:C.clear c2 e2
end of H11
we proceed by induction on H11 to prove ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abbr) u)
case ex_intro2 : x2:C H12:csubt g (CHead d1 (Bind Abbr) u) x2 H13:clear c2 x2 ⇒
the thesis becomes ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abbr) u)
(H14)
by (csubt_gen_abbr . . . . H12)
ex2 C λe2:C.eq C x2 (CHead e2 (Bind Abbr) u) λe2:C.csubt g d1 e2
end of H14
we proceed by induction on H14 to prove ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abbr) u)
case ex_intro2 : x3:C H15:eq C x2 (CHead x3 (Bind Abbr) u) H16:csubt g d1 x3 ⇒
the thesis becomes ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abbr) u)
(H17)
we proceed by induction on H15 to prove clear c2 (CHead x3 (Bind Abbr) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
clear c2 (CHead x3 (Bind Abbr) u)
end of H17
by (drop_refl .)
we proved drop O O c2 c2
by (getl_intro . . . . previous H17)
we proved getl O c2 (CHead x3 (Bind Abbr) u)
by (ex_intro2 . . . . H16 previous)
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abbr) u)
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abbr) u)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abbr) u)
∀x1:C
.drop O O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csubt g x1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl O c2 (CHead d2 (Bind Abbr) u)
case S : n0:nat ⇒
the thesis becomes
∀x1:C
.∀H9:drop (S n0) O x1 (CHead x0 (Flat f) t)
.∀c2:C
.∀H10:(csubt g x1 c2).(ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u))
(H8) by induction hypothesis we know
∀x1:C
.drop n0 O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csubt g x1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n0 c2 (CHead d2 (Bind Abbr) u)
assume x1: C
suppose H9: drop (S n0) O x1 (CHead x0 (Flat f) t)
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) t)
end of H11
we proceed by induction on H11 to prove ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
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) t) ⇒
the thesis becomes ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
(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 ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
case ex_intro2 : x5:C H15:csubt g (CHead x3 (Bind x2) x4) x5 H16:clear c2 x5 ⇒
the thesis becomes ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
(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 ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
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 ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
(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)
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n0 x7 (CHead d2 (Bind Abbr) u)
end of H21
we proceed by induction on H21 to prove ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
case ex_intro2 : x9:C H22:csubt g d1 x9 H23:getl n0 x7 (CHead x9 (Bind Abbr) u) ⇒
the thesis becomes ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
by (getl_clear_bind . . . . H20 . . H23)
we proved getl (S n0) c2 (CHead x9 (Bind Abbr) u)
by (ex_intro2 . . . . H22 previous)
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u)
∀x1:C
.∀H9:drop (S n0) O x1 (CHead x0 (Flat f) t)
.∀c2:C
.∀H10:(csubt g x1 c2).(ex2 C λd2:C.csubt g d1 d2 λd2:C.getl (S n0) c2 (CHead d2 (Bind Abbr) u))
we proved
∀x1:C
.drop n O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csubt g x1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
by (unintro . . . previous H7)
we proved
∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
∀H5:drop n O c1 (CHead x0 (Flat f) t)
.∀H6:clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abbr) u)
.∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
by (previous . H3 H4)
we proved
∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
∀H3:drop n O c1 (CHead x0 k t)
.∀H4:clear (CHead x0 k t) (CHead d1 (Bind Abbr) u)
.∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
by (previous . H1 H2)
∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
we proved
∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
we proved
∀g:G
.∀c1:C
.∀d1:C
.∀u:T
.∀n:nat
.getl n c1 (CHead d1 (Bind Abbr) u)
→∀c2:C
.csubt g c1 c2
→ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)