DEFINITION csubc_clear_conf()
TYPE =
∀g:G.∀c1:C.∀e1:C.(clear c1 e1)→∀c2:C.(csubc g c1 c2)→(ex2 C λe2:C.clear c2 e2 λe2:C.csubc g e1 e2)
BODY =
assume g: G
assume c1: C
assume e1: C
suppose H: clear c1 e1
we proceed by induction on H to prove ∀c2:C.(csubc g c1 c2)→(ex2 C λe2:C.clear c2 e2 λe2:C.csubc g e1 e2)
case clear_bind : b:B e:C u:T ⇒
the thesis becomes
∀c2:C
.∀H0:csubc g (CHead e (Bind b) u) c2
.ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
assume c2: C
suppose H0: csubc g (CHead e (Bind b) u) c2
(H_x)
by (csubc_gen_head_l . . . . . H0)
or3
ex2 C λc2:C.eq C c2 (CHead c2 (Bind b) u) λc2:C.csubc g e c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K (Bind b) (Bind Abst)
λc2:C.λw:T.λ:A.eq C c2 (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g e c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) e u
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C c2 (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K (Bind b) (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g e c2
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
case or3_intro0 : H2:ex2 C λc3:C.eq C c2 (CHead c3 (Bind b) u) λc3:C.csubc g e c3 ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
we proceed by induction on H2 to prove ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
case ex_intro2 : x:C H3:eq C c2 (CHead x (Bind b) u) H4:csubc g e x ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
(h1)
by (clear_bind . . .)
clear (CHead x (Bind b) u) (CHead x (Bind b) u)
end of h1
(h2)
by (csubc_head . . . H4 . .)
csubc g (CHead e (Bind b) u) (CHead x (Bind b) u)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
C
λe2:C.clear (CHead x (Bind b) u) e2
λe2:C.csubc g (CHead e (Bind b) u) e2
by (eq_ind_r . . . previous . H3)
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
case or3_intro1 : H2:ex5_3 C T A λ:C.λ:T.λ:A.eq K (Bind b) (Bind Abst) λc3:C.λw:T.λ:A.eq C c2 (CHead c3 (Bind Abbr) w) λc3:C.λ:T.λ:A.csubc g e c3 λ:C.λ:T.λa:A.sc3 g (asucc g a) e u λc3:C.λw:T.λa:A.sc3 g a c3 w ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
we proceed by induction on H2 to prove ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
case ex5_3_intro : x0:C x1:T x2:A H3:eq K (Bind b) (Bind Abst) H4:eq C c2 (CHead x0 (Bind Abbr) x1) H5:csubc g e x0 H6:sc3 g (asucc g x2) e u H7:sc3 g x2 x0 x1 ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
(H8)
by (f_equal . . . . . H3)
we proved
eq
B
<λ:K.B> CASE Bind b OF Bind b0⇒b0 | Flat ⇒b
<λ:K.B> CASE Bind Abst OF Bind b0⇒b0 | Flat ⇒b
eq
B
λe0:K.<λ:K.B> CASE e0 OF Bind b0⇒b0 | Flat ⇒b (Bind b)
λe0:K.<λ:K.B> CASE e0 OF Bind b0⇒b0 | Flat ⇒b (Bind Abst)
end of H8
(h1)
(h1)
by (clear_bind . . .)
clear (CHead x0 (Bind Abbr) x1) (CHead x0 (Bind Abbr) x1)
end of h1
(h2)
by (csubc_abst . . . H5 . . H6 . H7)
csubc g (CHead e (Bind Abst) u) (CHead x0 (Bind Abbr) x1)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λe2:C.clear (CHead x0 (Bind Abbr) x1) e2
λe2:C.csubc g (CHead e (Bind Abst) u) e2
end of h1
(h2)
consider H8
we proved
eq
B
<λ:K.B> CASE Bind b OF Bind b0⇒b0 | Flat ⇒b
<λ:K.B> CASE Bind Abst OF Bind b0⇒b0 | Flat ⇒b
eq B b Abst
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ex2
C
λe2:C.clear (CHead x0 (Bind Abbr) x1) e2
λe2:C.csubc g (CHead e (Bind b) u) e2
by (eq_ind_r . . . previous . H4)
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
case or3_intro2 : H2:ex4_3 B C T λb0:B.λc3:C.λv2:T.eq C c2 (CHead c3 (Bind b0) v2) λ:B.λ:C.λ:T.eq K (Bind b) (Bind Void) λb0:B.λ:C.λ:T.not (eq B b0 Void) λ:B.λc3:C.λ:T.csubc g e c3 ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
we proceed by induction on H2 to prove ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
case ex4_3_intro : x0:B x1:C x2:T H3:eq C c2 (CHead x1 (Bind x0) x2) H4:eq K (Bind b) (Bind Void) H5:not (eq B x0 Void) H6:csubc g e x1 ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
(H7)
by (f_equal . . . . . H4)
we proved
eq
B
<λ:K.B> CASE Bind b OF Bind b0⇒b0 | Flat ⇒b
<λ:K.B> CASE Bind Void OF Bind b0⇒b0 | Flat ⇒b
eq
B
λe0:K.<λ:K.B> CASE e0 OF Bind b0⇒b0 | Flat ⇒b (Bind b)
λe0:K.<λ:K.B> CASE e0 OF Bind b0⇒b0 | Flat ⇒b (Bind Void)
end of H7
(h1)
(h1)
by (clear_bind . . .)
clear (CHead x1 (Bind x0) x2) (CHead x1 (Bind x0) x2)
end of h1
(h2)
by (csubc_void . . . H6 . H5 . .)
csubc g (CHead e (Bind Void) u) (CHead x1 (Bind x0) x2)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λe2:C.clear (CHead x1 (Bind x0) x2) e2
λe2:C.csubc g (CHead e (Bind Void) u) e2
end of h1
(h2)
consider H7
we proved
eq
B
<λ:K.B> CASE Bind b OF Bind b0⇒b0 | Flat ⇒b
<λ:K.B> CASE Bind Void OF Bind b0⇒b0 | Flat ⇒b
eq B b Void
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ex2
C
λe2:C.clear (CHead x1 (Bind x0) x2) e2
λe2:C.csubc g (CHead e (Bind b) u) e2
by (eq_ind_r . . . previous . H3)
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
we proved ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
∀c2:C
.∀H0:csubc g (CHead e (Bind b) u) c2
.ex2 C λe2:C.clear c2 e2 λe2:C.csubc g (CHead e (Bind b) u) e2
case clear_flat : e:C c:C :clear e c f:F u:T ⇒
the thesis becomes ∀c2:C.∀H2:(csubc g (CHead e (Flat f) u) c2).(ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2)
(H1) by induction hypothesis we know ∀c2:C.(csubc g e c2)→(ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2)
assume c2: C
suppose H2: csubc g (CHead e (Flat f) u) c2
(H_x)
by (csubc_gen_head_l . . . . . H2)
or3
ex2 C λc2:C.eq C c2 (CHead c2 (Flat f) u) λc2:C.csubc g e c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K (Flat f) (Bind Abst)
λc2:C.λw:T.λ:A.eq C c2 (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g e c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) e u
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C c2 (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K (Flat f) (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g e c2
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
case or3_intro0 : H4:ex2 C λc3:C.eq C c2 (CHead c3 (Flat f) u) λc3:C.csubc g e c3 ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
we proceed by induction on H4 to prove ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
case ex_intro2 : x:C H5:eq C c2 (CHead x (Flat f) u) H6:csubc g e x ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
(H_x0)
by (H1 . H6)
ex2 C λe2:C.clear x e2 λe2:C.csubc g c e2
end of H_x0
(H7) consider H_x0
we proceed by induction on H7 to prove ex2 C λe2:C.clear (CHead x (Flat f) u) e2 λe2:C.csubc g c e2
case ex_intro2 : x0:C H8:clear x x0 H9:csubc g c x0 ⇒
the thesis becomes ex2 C λe2:C.clear (CHead x (Flat f) u) e2 λe2:C.csubc g c e2
by (clear_flat . . H8 . .)
we proved clear (CHead x (Flat f) u) x0
by (ex_intro2 . . . . previous H9)
ex2 C λe2:C.clear (CHead x (Flat f) u) e2 λe2:C.csubc g c e2
we proved ex2 C λe2:C.clear (CHead x (Flat f) u) e2 λe2:C.csubc g c e2
by (eq_ind_r . . . previous . H5)
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
case or3_intro1 : H4:ex5_3 C T A λ:C.λ:T.λ:A.eq K (Flat f) (Bind Abst) λc3:C.λw:T.λ:A.eq C c2 (CHead c3 (Bind Abbr) w) λc3:C.λ:T.λ:A.csubc g e c3 λ:C.λ:T.λa:A.sc3 g (asucc g a) e u λc3:C.λw:T.λa:A.sc3 g a c3 w ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
we proceed by induction on H4 to prove ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
case ex5_3_intro : x0:C x1:T x2:A H5:eq K (Flat f) (Bind Abst) H6:eq C c2 (CHead x0 (Bind Abbr) x1) :csubc g e x0 :sc3 g (asucc g x2) e u :sc3 g x2 x0 x1 ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
(H10)
we proceed by induction on H5 to prove <λ:K.Prop> CASE Bind Abst OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes <λ:K.Prop> CASE Flat f OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:K.Prop> CASE Flat f OF Bind ⇒False | Flat ⇒True
<λ:K.Prop> CASE Bind Abst OF Bind ⇒False | Flat ⇒True
end of H10
consider H10
we proved <λ:K.Prop> CASE Bind Abst OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove ex2 C λe2:C.clear (CHead x0 (Bind Abbr) x1) e2 λe2:C.csubc g c e2
we proved ex2 C λe2:C.clear (CHead x0 (Bind Abbr) x1) e2 λe2:C.csubc g c e2
by (eq_ind_r . . . previous . H6)
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
case or3_intro2 : H4:ex4_3 B C T λb:B.λc3:C.λv2:T.eq C c2 (CHead c3 (Bind b) v2) λ:B.λ:C.λ:T.eq K (Flat f) (Bind Void) λb:B.λ:C.λ:T.not (eq B b Void) λ:B.λc3:C.λ:T.csubc g e c3 ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
we proceed by induction on H4 to prove ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
case ex4_3_intro : x0:B x1:C x2:T H5:eq C c2 (CHead x1 (Bind x0) x2) H6:eq K (Flat f) (Bind Void) :not (eq B x0 Void) :csubc g e x1 ⇒
the thesis becomes ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
(H9)
we proceed by induction on H6 to prove <λ:K.Prop> CASE Bind Void OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes <λ:K.Prop> CASE Flat f OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:K.Prop> CASE Flat f OF Bind ⇒False | Flat ⇒True
<λ:K.Prop> CASE Bind Void OF Bind ⇒False | Flat ⇒True
end of H9
consider H9
we proved <λ:K.Prop> CASE Bind Void OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove ex2 C λe2:C.clear (CHead x1 (Bind x0) x2) e2 λe2:C.csubc g c e2
we proved ex2 C λe2:C.clear (CHead x1 (Bind x0) x2) e2 λe2:C.csubc g c e2
by (eq_ind_r . . . previous . H5)
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
we proved ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2
∀c2:C.∀H2:(csubc g (CHead e (Flat f) u) c2).(ex2 C λe2:C.clear c2 e2 λe2:C.csubc g c e2)
we proved ∀c2:C.(csubc g c1 c2)→(ex2 C λe2:C.clear c2 e2 λe2:C.csubc g e1 e2)
we proved
∀g:G.∀c1:C.∀e1:C.(clear c1 e1)→∀c2:C.(csubc g c1 c2)→(ex2 C λe2:C.clear c2 e2 λe2:C.csubc g e1 e2)