DEFINITION csuba_getl_abbr()
TYPE =
∀g:G
.∀c1:C
.∀d1:C
.∀u:T
.∀i:nat
.getl i c1 (CHead d1 (Bind Abbr) u)
→∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
BODY =
assume g: G
assume c1: C
assume d1: C
assume u: T
assume i: nat
suppose H: getl i c1 (CHead d1 (Bind Abbr) u)
(H0)
by (getl_gen_all . . . H)
ex2 C λe:C.drop i 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
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
case ex_intro2 : x:C H1:drop i O c1 x H2:clear x (CHead d1 (Bind Abbr) u) ⇒
the thesis becomes
∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
assume n: nat
suppose : drop i O c1 (CSort n)
suppose H4: clear (CSort n) (CHead d1 (Bind Abbr) u)
by (clear_gen_sort . . H4 .)
we proved
∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
drop i O c1 (CSort n)
→∀H4:clear (CSort n) (CHead d1 (Bind Abbr) u)
.∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
assume x0: C
suppose :
drop i O c1 x0
→(clear x0 (CHead d1 (Bind Abbr) u)
→∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2)
assume k: K
assume t: T
suppose H3: drop i O c1 (CHead x0 k t)
suppose H4: clear (CHead x0 k t) (CHead d1 (Bind Abbr) u)
assume b: B
suppose H5: drop i 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: csuba 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 i O c1 (CHead x0 (Bind b) u)
end of H13
(H14)
by (eq_ind_r . . . H13 . H10)
drop i O c1 (CHead x0 (Bind Abbr) u)
end of H14
(H15)
by (eq_ind_r . . . H14 . H11)
drop i O c1 (CHead d1 (Bind Abbr) u)
end of H15
(H16)
by (csuba_drop_abbr . . . . H15 . . H12)
ex2 C λd2:C.drop i O c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
end of H16
we proceed by induction on H16 to prove ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
case ex_intro2 : x1:C H17:drop i O c2 (CHead x1 (Bind Abbr) u) H18:csuba g d1 x1 ⇒
the thesis becomes ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
by (clear_bind . . .)
we proved clear (CHead x1 (Bind Abbr) u) (CHead x1 (Bind Abbr) u)
by (getl_intro . . . . H17 previous)
we proved getl i c2 (CHead x1 (Bind Abbr) u)
by (ex_intro2 . . . . previous H18)
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
we proved ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
eq B Abbr b
→(eq C d1 x0
→∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2)
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
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
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
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
∀H5:drop i O c1 (CHead x0 (Bind b) t)
.∀H6:clear (CHead x0 (Bind b) t) (CHead d1 (Bind Abbr) u)
.∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
assume f: F
suppose H5: drop i 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 i to prove
∀x1:C
.drop i O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g x1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
case O : ⇒
the thesis becomes
∀x1:C
.drop O O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g x1 c2
→ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
assume x1: C
suppose H8: drop O O x1 (CHead x0 (Flat f) t)
assume c2: C
suppose H9: csuba 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 csuba g (CHead x0 (Flat f) t) c2
case refl_equal : ⇒
the thesis becomes the hypothesis H9
csuba 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 (csuba_clear_conf . . . H10 . H_y)
ex2 C λe2:C.csuba 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.getl O c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
case ex_intro2 : x2:C H12:csuba g (CHead d1 (Bind Abbr) u) x2 H13:clear c2 x2 ⇒
the thesis becomes ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
(H_x)
by (csuba_gen_abbr . . . . H12)
ex2 C λd2:C.eq C x2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
end of H_x
(H14) consider H_x
we proceed by induction on H14 to prove ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
case ex_intro2 : x3:C H15:eq C x2 (CHead x3 (Bind Abbr) u) H16:csuba g d1 x3 ⇒
the thesis becomes ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
(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 . . . . previous H16)
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
we proved ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
∀x1:C
.drop O O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g x1 c2
→ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
case S : n:nat ⇒
the thesis becomes
∀x1:C
.∀H9:drop (S n) O x1 (CHead x0 (Flat f) t)
.∀c2:C
.∀H10:csuba g x1 c2
.ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
(H8) by induction hypothesis we know
∀x1:C
.drop n O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g x1 c2
→ex2 C λd2:C.getl n c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
assume x1: C
suppose H9: drop (S n) O x1 (CHead x0 (Flat f) t)
assume c2: C
suppose H10: csuba 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 n O e (CHead x0 (Flat f) t)
end of H11
we proceed by induction on H11 to prove ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
case ex2_3_intro : x2:B x3:C x4:T H12:clear x1 (CHead x3 (Bind x2) x4) H13:drop n O x3 (CHead x0 (Flat f) t) ⇒
the thesis becomes ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
(H14)
by (csuba_clear_conf . . . H10 . H12)
ex2 C λe2:C.csuba 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.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
case ex_intro2 : x5:C H15:csuba g (CHead x3 (Bind x2) x4) x5 H16:clear c2 x5 ⇒
the thesis becomes ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
(H_x)
by (csuba_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.csuba g x3 e2
end of H_x
(H17) consider H_x
we proceed by induction on H17 to prove ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
case ex2_3_intro : x6:B x7:C x8:T H18:eq C x5 (CHead x7 (Bind x6) x8) H19:csuba g x3 x7 ⇒
the thesis becomes ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
(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.getl n x7 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
end of H21
we proceed by induction on H21 to prove ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
case ex_intro2 : x9:C H22:getl n x7 (CHead x9 (Bind Abbr) u) H23:csuba g d1 x9 ⇒
the thesis becomes ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
by (getl_clear_bind . . . . H20 . . H22)
we proved getl (S n) c2 (CHead x9 (Bind Abbr) u)
by (ex_intro2 . . . . previous H23)
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
we proved ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
∀x1:C
.∀H9:drop (S n) O x1 (CHead x0 (Flat f) t)
.∀c2:C
.∀H10:csuba g x1 c2
.ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
we proved
∀x1:C
.drop i O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g x1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
by (unintro . . . previous H7)
we proved
∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
∀H5:drop i O c1 (CHead x0 (Flat f) t)
.∀H6:clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abbr) u)
.∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
by (previous . H3 H4)
we proved
∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
∀H3:drop i O c1 (CHead x0 k t)
.∀H4:clear (CHead x0 k t) (CHead d1 (Bind Abbr) u)
.∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
by (previous . H1 H2)
∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
we proved
∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
we proved
∀g:G
.∀c1:C
.∀d1:C
.∀u:T
.∀i:nat
.getl i c1 (CHead d1 (Bind Abbr) u)
→∀c2:C
.csuba g c1 c2
→ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2