DEFINITION csuba_getl_abst_rev()
TYPE =
∀g:G
.∀c1:C
.∀d1:C
.∀u:T
.∀i:nat
.getl i c1 (CHead d1 (Bind Abst) u)
→∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
BODY =
assume g: G
assume c1: C
assume d1: C
assume u: T
assume i: nat
suppose H: getl i c1 (CHead d1 (Bind Abst) u)
(H0)
by (getl_gen_all . . . H)
ex2 C λe:C.drop i O c1 e λe:C.clear e (CHead d1 (Bind Abst) u)
end of H0
we proceed by induction on H0 to prove
∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
case ex_intro2 : x:C H1:drop i O c1 x H2:clear x (CHead d1 (Bind Abst) u) ⇒
the thesis becomes
∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
assume n: nat
suppose : drop i O c1 (CSort n)
suppose H4: clear (CSort n) (CHead d1 (Bind Abst) u)
by (clear_gen_sort . . H4 .)
we proved
∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
drop i O c1 (CSort n)
→∀H4:clear (CSort n) (CHead d1 (Bind Abst) u)
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
assume x0: C
suppose :
drop i O c1 x0
→(clear x0 (CHead d1 (Bind Abst) u)
→∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1))
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 Abst) 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 Abst) u)
(H7)
by (clear_gen_bind . . . . H6)
we proved eq C (CHead d1 (Bind Abst) u) (CHead x0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Abst) 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 Abst) 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 Abst) u) (CHead x0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind Abst) u OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
<λ:C.B>
CASE CHead x0 (Bind b) t 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) u
λ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) t
end of H8
(h1)
(H9)
by (clear_gen_bind . . . . H6)
we proved eq C (CHead d1 (Bind Abst) u) (CHead x0 (Bind b) t)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d1 (Bind Abst) 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 Abst) 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 Abst b
suppose H11: eq C d1 x0
assume c2: C
suppose H12: csuba g c2 c1
(H13)
consider H9
we proved
eq
T
<λ:C.T> CASE CHead d1 (Bind Abst) 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 Abst) u)
end of H14
(H15)
by (eq_ind_r . . . H14 . H11)
drop i O c1 (CHead d1 (Bind Abst) u)
end of H15
(H16)
by (csuba_drop_abst_rev . . . . H15 . . H12)
or
ex2 C λd2:C.drop i O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop i O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of H16
we proceed by induction on H16 to prove
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or_introl : H17:ex2 C λd2:C.drop i O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H17 to prove
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x1:C H18:drop i O c2 (CHead x1 (Bind Abst) u) H19:csuba g x1 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
by (clear_bind . . .)
we proved clear (CHead x1 (Bind Abst) u) (CHead x1 (Bind Abst) u)
by (getl_intro . . . . H18 previous)
we proved getl i c2 (CHead x1 (Bind Abst) u)
by (ex_intro2 . . . . previous H19)
we proved ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
by (or_introl . . previous)
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or_intror : H17:ex2_2 C T λd2:C.λu2:T.drop i O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H17 to prove
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x1:C x2:T H18:drop i O c2 (CHead x1 (Bind Void) x2) H19:csuba g x1 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
by (clear_bind . . .)
we proved clear (CHead x1 (Bind Void) x2) (CHead x1 (Bind Void) x2)
by (getl_intro . . . . H18 previous)
we proved getl i c2 (CHead x1 (Bind Void) x2)
by (ex2_2_intro . . . . . . previous H19)
we proved ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
by (or_intror . . previous)
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
eq B Abst b
→(eq C d1 x0
→∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1))
end of h1
(h2)
consider H8
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind Abst) u OF
CSort ⇒Abst
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abst
<λ:C.B>
CASE CHead x0 (Bind b) t 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
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
end of h1
(h2)
consider H7
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Abst) 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 c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
∀H5:drop i O c1 (CHead x0 (Bind b) t)
.∀H6:clear (CHead x0 (Bind b) t) (CHead d1 (Bind Abst) u)
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
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 Abst) 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 c2 x1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
case O : ⇒
the thesis becomes
∀x1:C
.drop O O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g c2 x1
→(or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
assume x1: C
suppose H8: drop O O x1 (CHead x0 (Flat f) t)
assume c2: C
suppose H9: csuba g c2 x1
(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 c2 (CHead x0 (Flat f) t)
case refl_equal : ⇒
the thesis becomes the hypothesis H9
csuba g c2 (CHead x0 (Flat f) t)
end of H10
(H_y)
by (clear_gen_flat . . . . H6)
we proved clear x0 (CHead d1 (Bind Abst) u)
by (clear_flat . . previous . .)
clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abst) u)
end of H_y
(H11)
by (csuba_clear_trans . . . H10 . H_y)
ex2 C λe2:C.csuba g e2 (CHead d1 (Bind Abst) u) λe2:C.clear c2 e2
end of H11
we proceed by induction on H11 to prove
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x2:C H12:csuba g x2 (CHead d1 (Bind Abst) u) H13:clear c2 x2 ⇒
the thesis becomes
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H_x)
by (csuba_gen_abst_rev . . . . H12)
or
ex2 C λd2:C.eq C x2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.eq C x2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of H_x
(H14) consider H_x
we proceed by induction on H14 to prove
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or_introl : H15:ex2 C λd2:C.eq C x2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H15 to prove
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x3:C H16:eq C x2 (CHead x3 (Bind Abst) u) H17:csuba g x3 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H18)
we proceed by induction on H16 to prove clear c2 (CHead x3 (Bind Abst) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
clear c2 (CHead x3 (Bind Abst) u)
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) u)
by (ex_intro2 . . . . previous H17)
we proved ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
by (or_introl . . previous)
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or_intror : H15:ex2_2 C T λd2:C.λu2:T.eq C x2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H15 to prove
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x3:C x4:T H16:eq C x2 (CHead x3 (Bind Void) x4) H17:csuba g x3 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H18)
we proceed by induction on H16 to prove clear c2 (CHead x3 (Bind Void) x4)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
clear c2 (CHead x3 (Bind Void) x4)
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 Void) x4)
by (ex2_2_intro . . . . . . previous H17)
we proved ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
by (or_intror . . previous)
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
∀x1:C
.drop O O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g c2 x1
→(or
ex2 C λd2:C.getl O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
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 c2 x1
.or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H8) by induction hypothesis we know
∀x1:C
.drop n O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g c2 x1
→(or
ex2 C λd2:C.getl n c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl n c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
assume x1: C
suppose H9: drop (S n) O x1 (CHead x0 (Flat f) t)
assume c2: C
suppose H10: csuba g c2 x1
(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
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
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
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H14)
by (csuba_clear_trans . . . H10 . H12)
ex2 C λe2:C.csuba g e2 (CHead x3 (Bind x2) x4) λe2:C.clear c2 e2
end of H14
we proceed by induction on H14 to prove
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x5:C H15:csuba g x5 (CHead x3 (Bind x2) x4) H16:clear c2 x5 ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H_x)
by (csuba_gen_bind_rev . . . . . 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 e2 x3
end of H_x
(H17) consider H_x
we proceed by induction on H17 to prove
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex2_3_intro : x6:B x7:C x8:T H18:eq C x5 (CHead x7 (Bind x6) x8) H19:csuba g x7 x3 ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(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.getl n x7 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl n x7 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of H21
we proceed by induction on H21 to prove
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or_introl : H22:ex2 C λd2:C.getl n x7 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H22 to prove
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x9:C H23:getl n x7 (CHead x9 (Bind Abst) u) H24:csuba g x9 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
by (getl_clear_bind . . . . H20 . . H23)
we proved getl (S n) c2 (CHead x9 (Bind Abst) u)
by (ex_intro2 . . . . previous H24)
we proved ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
by (or_introl . . previous)
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or_intror : H22:ex2_2 C T λd2:C.λu2:T.getl n x7 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H22 to prove
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x9:C x10:T H23:getl n x7 (CHead x9 (Bind Void) x10) H24:csuba g x9 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
by (getl_clear_bind . . . . H20 . . H23)
we proved getl (S n) c2 (CHead x9 (Bind Void) x10)
by (ex2_2_intro . . . . . . previous H24)
we proved ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
by (or_intror . . previous)
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
∀x1:C
.∀H9:drop (S n) O x1 (CHead x0 (Flat f) t)
.∀c2:C
.∀H10:csuba g c2 x1
.or
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl (S n) c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
∀x1:C
.drop i O x1 (CHead x0 (Flat f) t)
→∀c2:C
.csuba g c2 x1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
by (unintro . . . previous H7)
we proved
∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
∀H5:drop i O c1 (CHead x0 (Flat f) t)
.∀H6:clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abst) u)
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
by (previous . H3 H4)
we proved
∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
∀H3:drop i O c1 (CHead x0 k t)
.∀H4:clear (CHead x0 k t) (CHead d1 (Bind Abst) u)
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
by (previous . H1 H2)
∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
we proved
∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
we proved
∀g:G
.∀c1:C
.∀d1:C
.∀u:T
.∀i:nat
.getl i c1 (CHead d1 (Bind Abst) u)
→∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)