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