DEFINITION clear_ctail()
TYPE =
∀b:B
.∀c1:C
.∀c2:C
.∀u2:T
.clear c1 (CHead c2 (Bind b) u2)
→∀k:K.∀u1:T.(clear (CTail k u1 c1) (CHead (CTail k u1 c2) (Bind b) u2))
BODY =
assume b: B
assume c1: C
we proceed by induction on c1 to prove
∀c2:C
.∀u2:T
.clear c1 (CHead c2 (Bind b) u2)
→∀k:K.∀u1:T.(clear (CTail k u1 c1) (CHead (CTail k u1 c2) (Bind b) u2))
case CSort : n:nat ⇒
the thesis becomes
∀c2:C
.∀u2:T
.∀H:clear (CSort n) (CHead c2 (Bind b) u2)
.∀k:K.∀u1:T.(clear (CHead (CSort n) k u1) (CHead (CTail k u1 c2) (Bind b) u2))
assume c2: C
assume u2: T
suppose H: clear (CSort n) (CHead c2 (Bind b) u2)
assume k: K
assume u1: T
we proceed by induction on k to prove clear (CHead (CSort n) k u1) (CHead (CTail k u1 c2) (Bind b) u2)
case Bind : b0:B ⇒
the thesis becomes
clear
CHead (CSort n) (Bind b0) u1
CHead (CTail (Bind b0) u1 c2) (Bind b) u2
by (clear_gen_sort . . H .)
clear
CHead (CSort n) (Bind b0) u1
CHead (CTail (Bind b0) u1 c2) (Bind b) u2
case Flat : f:F ⇒
the thesis becomes
clear
CHead (CSort n) (Flat f) u1
CHead (CTail (Flat f) u1 c2) (Bind b) u2
by (clear_gen_sort . . H .)
clear
CHead (CSort n) (Flat f) u1
CHead (CTail (Flat f) u1 c2) (Bind b) u2
we proved clear (CHead (CSort n) k u1) (CHead (CTail k u1 c2) (Bind b) u2)
that is equivalent to clear (CTail k u1 (CSort n)) (CHead (CTail k u1 c2) (Bind b) u2)
∀c2:C
.∀u2:T
.∀H:clear (CSort n) (CHead c2 (Bind b) u2)
.∀k:K.∀u1:T.(clear (CHead (CSort n) k u1) (CHead (CTail k u1 c2) (Bind b) u2))
case CHead : c:C k:K t:T ⇒
the thesis becomes
∀c2:C
.∀u2:T
.∀H0:clear (CHead c k t) (CHead c2 (Bind b) u2)
.∀k0:K.∀u1:T.(clear (CHead (CTail k0 u1 c) k t) (CHead (CTail k0 u1 c2) (Bind b) u2))
(H) by induction hypothesis we know
∀c2:C
.∀u2:T
.clear c (CHead c2 (Bind b) u2)
→∀k:K.∀u1:T.(clear (CTail k u1 c) (CHead (CTail k u1 c2) (Bind b) u2))
assume c2: C
assume u2: T
suppose H0: clear (CHead c k t) (CHead c2 (Bind b) u2)
assume k0: K
assume u1: T
assume b0: B
suppose H1: clear (CHead c (Bind b0) t) (CHead c2 (Bind b) u2)
(H2)
by (clear_gen_bind . . . . H1)
we proved eq C (CHead c2 (Bind b) u2) (CHead c (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c (Bind b0) t OF CSort ⇒c2 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead c2 (Bind b) u2)
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead c (Bind b0) t)
end of H2
(h1)
(H3)
by (clear_gen_bind . . . . H1)
we proved eq C (CHead c2 (Bind b) u2) (CHead c (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead c2 (Bind b) u2 OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead c (Bind b0) t OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
eq
B
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
CHead c2 (Bind b) u2
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
CHead c (Bind b0) t
end of H3
(h1)
(H4)
by (clear_gen_bind . . . . H1)
we proved eq C (CHead c2 (Bind b) u2) (CHead c (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead c2 (Bind b) u2 OF CSort ⇒u2 | CHead t0⇒t0
<λ:C.T> CASE CHead c (Bind b0) t OF CSort ⇒u2 | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t0⇒t0 (CHead c2 (Bind b) u2)
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t0⇒t0 (CHead c (Bind b0) t)
end of H4
suppose H5: eq B b b0
suppose H6: eq C c2 c
(h1)
we proceed by induction on H5 to prove
clear
CHead (CTail k0 u1 c) (Bind b0) t
CHead (CTail k0 u1 c) (Bind b) t
case refl_equal : ⇒
the thesis becomes
clear
CHead (CTail k0 u1 c) (Bind b) t
CHead (CTail k0 u1 c) (Bind b) t
by (clear_bind . . .)
clear
CHead (CTail k0 u1 c) (Bind b) t
CHead (CTail k0 u1 c) (Bind b) t
we proved
clear
CHead (CTail k0 u1 c) (Bind b0) t
CHead (CTail k0 u1 c) (Bind b) t
by (eq_ind_r . . . previous . H6)
clear
CHead (CTail k0 u1 c) (Bind b0) t
CHead (CTail k0 u1 c2) (Bind b) t
end of h1
(h2)
consider H4
we proved
eq
T
<λ:C.T> CASE CHead c2 (Bind b) u2 OF CSort ⇒u2 | CHead t0⇒t0
<λ:C.T> CASE CHead c (Bind b0) t OF CSort ⇒u2 | CHead t0⇒t0
eq T u2 t
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
clear
CHead (CTail k0 u1 c) (Bind b0) t
CHead (CTail k0 u1 c2) (Bind b) u2
eq B b b0
→(eq C c2 c
→(clear
CHead (CTail k0 u1 c) (Bind b0) t
CHead (CTail k0 u1 c2) (Bind b) u2))
end of h1
(h2)
consider H3
we proved
eq
B
<λ:C.B>
CASE CHead c2 (Bind b) u2 OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead c (Bind b0) t OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
eq B b b0
end of h2
by (h1 h2)
eq C c2 c
→(clear
CHead (CTail k0 u1 c) (Bind b0) t
CHead (CTail k0 u1 c2) (Bind b) u2)
end of h1
(h2)
consider H2
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c (Bind b0) t OF CSort ⇒c2 | CHead c0 ⇒c0
eq C c2 c
end of h2
by (h1 h2)
we proved
clear
CHead (CTail k0 u1 c) (Bind b0) t
CHead (CTail k0 u1 c2) (Bind b) u2
∀H1:clear (CHead c (Bind b0) t) (CHead c2 (Bind b) u2)
.clear
CHead (CTail k0 u1 c) (Bind b0) t
CHead (CTail k0 u1 c2) (Bind b) u2
assume f: F
suppose H1: clear (CHead c (Flat f) t) (CHead c2 (Bind b) u2)
by (clear_gen_flat . . . . H1)
we proved clear c (CHead c2 (Bind b) u2)
by (H . . previous . .)
we proved clear (CTail k0 u1 c) (CHead (CTail k0 u1 c2) (Bind b) u2)
by (clear_flat . . previous . .)
we proved
clear
CHead (CTail k0 u1 c) (Flat f) t
CHead (CTail k0 u1 c2) (Bind b) u2
∀H1:clear (CHead c (Flat f) t) (CHead c2 (Bind b) u2)
.clear
CHead (CTail k0 u1 c) (Flat f) t
CHead (CTail k0 u1 c2) (Bind b) u2
by (previous . H0)
we proved clear (CHead (CTail k0 u1 c) k t) (CHead (CTail k0 u1 c2) (Bind b) u2)
that is equivalent to clear (CTail k0 u1 (CHead c k t)) (CHead (CTail k0 u1 c2) (Bind b) u2)
∀c2:C
.∀u2:T
.∀H0:clear (CHead c k t) (CHead c2 (Bind b) u2)
.∀k0:K.∀u1:T.(clear (CHead (CTail k0 u1 c) k t) (CHead (CTail k0 u1 c2) (Bind b) u2))
we proved
∀c2:C
.∀u2:T
.clear c1 (CHead c2 (Bind b) u2)
→∀k:K.∀u1:T.(clear (CTail k u1 c1) (CHead (CTail k u1 c2) (Bind b) u2))
we proved
∀b:B
.∀c1:C
.∀c2:C
.∀u2:T
.clear c1 (CHead c2 (Bind b) u2)
→∀k:K.∀u1:T.(clear (CTail k u1 c1) (CHead (CTail k u1 c2) (Bind b) u2))