DEFINITION csubv_clear_conf_void()
TYPE =
∀c1:C
.∀c2:C
.csubv c1 c2
→∀d1:C
.∀v1:T
.clear c1 (CHead d1 (Bind Void) v1)
→ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear c2 (CHead d2 (Bind Void) v2)
BODY =
assume c1: C
assume c2: C
suppose H: csubv c1 c2
we proceed by induction on H to prove
∀d1:C
.∀v1:T
.clear c1 (CHead d1 (Bind Void) v1)
→ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear c2 (CHead d2 (Bind Void) v2)
case csubv_sort : n:nat ⇒
the thesis becomes
∀d1:C
.∀v1:T
.∀H0:clear (CSort n) (CHead d1 (Bind Void) v1)
.ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear (CSort n) (CHead d2 (Bind Void) v2)
assume d1: C
assume v1: T
suppose H0: clear (CSort n) (CHead d1 (Bind Void) v1)
by (clear_gen_sort . . H0 .)
we proved ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear (CSort n) (CHead d2 (Bind Void) v2)
∀d1:C
.∀v1:T
.∀H0:clear (CSort n) (CHead d1 (Bind Void) v1)
.ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear (CSort n) (CHead d2 (Bind Void) v2)
case csubv_void : c3:C c4:C H0:csubv c3 c4 v1:T v2:T ⇒
the thesis becomes
∀d1:C
.∀v0:T
.∀H2:clear (CHead c3 (Bind Void) v1) (CHead d1 (Bind Void) v0)
.ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Bind Void) v2) (CHead d2 (Bind Void) v3)
() by induction hypothesis we know
∀d1:C
.∀v1:T
.clear c3 (CHead d1 (Bind Void) v1)
→ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear c4 (CHead d2 (Bind Void) v2)
assume d1: C
assume v0: T
suppose H2: clear (CHead c3 (Bind Void) v1) (CHead d1 (Bind Void) v0)
(H3)
by (clear_gen_bind . . . . H2)
we proved eq C (CHead d1 (Bind Void) v0) (CHead c3 (Bind Void) v1)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Void) v0 OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead c3 (Bind Void) v1 OF CSort ⇒d1 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead d1 (Bind Void) v0)
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead c3 (Bind Void) v1)
end of H3
(H5)
consider H3
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Void) v0 OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead c3 (Bind Void) v1 OF CSort ⇒d1 | CHead c ⇒c
eq C d1 c3
end of H5
by (clear_bind . . .)
we proved clear (CHead c4 (Bind Void) v2) (CHead c4 (Bind Void) v2)
by (ex2_2_intro . . . . . . H0 previous)
we proved
ex2_2
C
T
λd2:C.λ:T.csubv c3 d2
λd2:C.λv3:T.clear (CHead c4 (Bind Void) v2) (CHead d2 (Bind Void) v3)
by (eq_ind_r . . . previous . H5)
we proved
ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Bind Void) v2) (CHead d2 (Bind Void) v3)
∀d1:C
.∀v0:T
.∀H2:clear (CHead c3 (Bind Void) v1) (CHead d1 (Bind Void) v0)
.ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Bind Void) v2) (CHead d2 (Bind Void) v3)
case csubv_bind : c3:C c4:C :csubv c3 c4 b1:B H2:not (eq B b1 Void) b2:B v1:T v2:T ⇒
the thesis becomes
∀d1:C
.∀v0:T
.∀H3:clear (CHead c3 (Bind b1) v1) (CHead d1 (Bind Void) v0)
.ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)
() by induction hypothesis we know
∀d1:C
.∀v1:T
.clear c3 (CHead d1 (Bind Void) v1)
→ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear c4 (CHead d2 (Bind Void) v2)
assume d1: C
assume v0: T
suppose H3: clear (CHead c3 (Bind b1) v1) (CHead d1 (Bind Void) v0)
(H4)
by (clear_gen_bind . . . . H3)
we proved eq C (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Void) v0 OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead c3 (Bind b1) v1 OF CSort ⇒d1 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead d1 (Bind Void) v0)
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead c3 (Bind b1) v1)
end of H4
(h1)
(H5)
by (clear_gen_bind . . . . H3)
we proved eq C (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind Void) v0 OF
CSort ⇒Void
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Void
<λ:C.B>
CASE CHead c3 (Bind b1) v1 OF
CSort ⇒Void
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Void
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Void
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Void
CHead d1 (Bind Void) v0
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Void
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Void
CHead c3 (Bind b1) v1
end of H5
(H7)
consider H5
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind Void) v0 OF
CSort ⇒Void
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Void
<λ:C.B>
CASE CHead c3 (Bind b1) v1 OF
CSort ⇒Void
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Void
eq B Void b1
end of H7
suppose H8: eq C d1 c3
(H9)
by (eq_ind_r . . . H2 . H7)
not (eq B Void Void)
end of H9
(H10)
by (refl_equal . .)
we proved eq B Void Void
by (H9 previous)
we proved False
by cases on the previous result we prove
ex2_2
C
T
λd2:C.λ:T.csubv c3 d2
λd2:C.λv3:T.clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)
ex2_2
C
T
λd2:C.λ:T.csubv c3 d2
λd2:C.λv3:T.clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)
end of H10
consider H10
we proved
ex2_2
C
T
λd2:C.λ:T.csubv c3 d2
λd2:C.λv3:T.clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)
by (eq_ind_r . . . previous . H8)
we proved
ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)
eq C d1 c3
→(ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3))
end of h1
(h2)
consider H4
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind Void) v0 OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead c3 (Bind b1) v1 OF CSort ⇒d1 | CHead c ⇒c
eq C d1 c3
end of h2
by (h1 h2)
we proved
ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)
∀d1:C
.∀v0:T
.∀H3:clear (CHead c3 (Bind b1) v1) (CHead d1 (Bind Void) v0)
.ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)
case csubv_flat : c3:C c4:C :csubv c3 c4 f1:F f2:F v1:T v2:T ⇒
the thesis becomes
∀d1:C
.∀v0:T
.∀H2:clear (CHead c3 (Flat f1) v1) (CHead d1 (Bind Void) v0)
.ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3)
(H1) by induction hypothesis we know
∀d1:C
.∀v1:T
.clear c3 (CHead d1 (Bind Void) v1)
→ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear c4 (CHead d2 (Bind Void) v2)
assume d1: C
assume v0: T
suppose H2: clear (CHead c3 (Flat f1) v1) (CHead d1 (Bind Void) v0)
(H_x)
by (clear_gen_flat . . . . H2)
we proved clear c3 (CHead d1 (Bind Void) v0)
by (H1 . . previous)
ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear c4 (CHead d2 (Bind Void) v2)
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove
ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3)
case ex2_2_intro : x0:C x1:T H4:csubv d1 x0 H5:clear c4 (CHead x0 (Bind Void) x1) ⇒
the thesis becomes
ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3)
by (clear_flat . . H5 . .)
we proved clear (CHead c4 (Flat f2) v2) (CHead x0 (Bind Void) x1)
by (ex2_2_intro . . . . . . H4 previous)
ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3)
we proved
ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3)
∀d1:C
.∀v0:T
.∀H2:clear (CHead c3 (Flat f1) v1) (CHead d1 (Bind Void) v0)
.ex2_2
C
T
λd2:C.λ:T.csubv d1 d2
λd2:C.λv3:T.clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3)
we proved
∀d1:C
.∀v1:T
.clear c1 (CHead d1 (Bind Void) v1)
→ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear c2 (CHead d2 (Bind Void) v2)
we proved
∀c1:C
.∀c2:C
.csubv c1 c2
→∀d1:C
.∀v1:T
.clear c1 (CHead d1 (Bind Void) v1)
→ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear c2 (CHead d2 (Bind Void) v2)