DEFINITION clear_gen_bind()
TYPE =
∀b:B
.∀e:C
.∀x:C
.∀u:T
.clear (CHead e (Bind b) u) x
→eq C x (CHead e (Bind b) u)
BODY =
assume b: B
assume e: C
assume x: C
assume u: T
suppose H: clear (CHead e (Bind b) u) x
assume y: C
suppose H0: clear y x
we proceed by induction on H0 to prove (eq C y (CHead e (Bind b) u))→(eq C x y)
case clear_bind : b0:B e0:C u0:T ⇒
the thesis becomes
∀H1:eq C (CHead e0 (Bind b0) u0) (CHead e (Bind b) u)
.eq C (CHead e0 (Bind b0) u0) (CHead e0 (Bind b0) u0)
suppose H1: eq C (CHead e0 (Bind b0) u0) (CHead e (Bind b) u)
(H2)
by (f_equal . . . . . H1)
we proved
eq
C
<λ:C.C> CASE CHead e0 (Bind b0) u0 OF CSort ⇒e0 | CHead c ⇒c
<λ:C.C> CASE CHead e (Bind b) u OF CSort ⇒e0 | CHead c ⇒c
eq
C
λe1:C.<λ:C.C> CASE e1 OF CSort ⇒e0 | CHead c ⇒c (CHead e0 (Bind b0) u0)
λe1:C.<λ:C.C> CASE e1 OF CSort ⇒e0 | CHead c ⇒c (CHead e (Bind b) u)
end of H2
(h1)
(H3)
by (f_equal . . . . . H1)
we proved
eq
B
<λ:C.B>
CASE CHead e0 (Bind b0) u0 OF
CSort ⇒b0
| CHead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
<λ:C.B>
CASE CHead e (Bind b) u OF
CSort ⇒b0
| CHead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
eq
B
λe1:C.<λ:C.B> CASE e1 OF CSort ⇒b0 | CHead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
CHead e0 (Bind b0) u0
λe1:C.<λ:C.B> CASE e1 OF CSort ⇒b0 | CHead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
CHead e (Bind b) u
end of H3
(h1)
(H4)
by (f_equal . . . . . H1)
we proved
eq
T
<λ:C.T> CASE CHead e0 (Bind b0) u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead e (Bind b) u OF CSort ⇒u0 | CHead t⇒t
eq
T
λe1:C.<λ:C.T> CASE e1 OF CSort ⇒u0 | CHead t⇒t (CHead e0 (Bind b0) u0)
λe1:C.<λ:C.T> CASE e1 OF CSort ⇒u0 | CHead t⇒t (CHead e (Bind b) u)
end of H4
suppose H5: eq B b0 b
suppose H6: eq C e0 e
(h1)
by (refl_equal . .)
we proved eq C (CHead e (Bind b) u) (CHead e (Bind b) u)
by (eq_ind_r . . . previous . H5)
we proved eq C (CHead e (Bind b0) u) (CHead e (Bind b0) u)
by (eq_ind_r . . . previous . H6)
eq C (CHead e0 (Bind b0) u) (CHead e0 (Bind b0) u)
end of h1
(h2)
consider H4
we proved
eq
T
<λ:C.T> CASE CHead e0 (Bind b0) u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead e (Bind b) u OF CSort ⇒u0 | CHead t⇒t
eq T u0 u
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq C (CHead e0 (Bind b0) u0) (CHead e0 (Bind b0) u0)
eq B b0 b
→(eq C e0 e)→(eq C (CHead e0 (Bind b0) u0) (CHead e0 (Bind b0) u0))
end of h1
(h2)
consider H3
we proved
eq
B
<λ:C.B>
CASE CHead e0 (Bind b0) u0 OF
CSort ⇒b0
| CHead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
<λ:C.B>
CASE CHead e (Bind b) u OF
CSort ⇒b0
| CHead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
eq B b0 b
end of h2
by (h1 h2)
(eq C e0 e)→(eq C (CHead e0 (Bind b0) u0) (CHead e0 (Bind b0) u0))
end of h1
(h2)
consider H2
we proved
eq
C
<λ:C.C> CASE CHead e0 (Bind b0) u0 OF CSort ⇒e0 | CHead c ⇒c
<λ:C.C> CASE CHead e (Bind b) u OF CSort ⇒e0 | CHead c ⇒c
eq C e0 e
end of h2
by (h1 h2)
we proved eq C (CHead e0 (Bind b0) u0) (CHead e0 (Bind b0) u0)
∀H1:eq C (CHead e0 (Bind b0) u0) (CHead e (Bind b) u)
.eq C (CHead e0 (Bind b0) u0) (CHead e0 (Bind b0) u0)
case clear_flat : e0:C c:C :clear e0 c f:F u0:T ⇒
the thesis becomes
∀H3:eq C (CHead e0 (Flat f) u0) (CHead e (Bind b) u)
.eq C c (CHead e0 (Flat f) u0)
() by induction hypothesis we know (eq C e0 (CHead e (Bind b) u))→(eq C c e0)
suppose H3: eq C (CHead e0 (Flat f) u0) (CHead e (Bind b) u)
(H4)
we proceed by induction on H3 to prove
<λ:C.Prop>
CASE CHead e (Bind b) u OF
CSort ⇒False
| CHead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead e0 (Flat f) u0 OF
CSort ⇒False
| CHead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:C.Prop>
CASE CHead e0 (Flat f) u0 OF
CSort ⇒False
| CHead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:C.Prop>
CASE CHead e (Bind b) u OF
CSort ⇒False
| CHead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
end of H4
consider H4
we proved
<λ:C.Prop>
CASE CHead e (Bind b) u OF
CSort ⇒False
| CHead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove eq C c (CHead e0 (Flat f) u0)
we proved eq C c (CHead e0 (Flat f) u0)
∀H3:eq C (CHead e0 (Flat f) u0) (CHead e (Bind b) u)
.eq C c (CHead e0 (Flat f) u0)
we proved (eq C y (CHead e (Bind b) u))→(eq C x y)
we proved
∀y:C.(clear y x)→(eq C y (CHead e (Bind b) u))→(eq C x y)
by (insert_eq . . . . previous H)
we proved eq C x (CHead e (Bind b) u)
we proved
∀b:B
.∀e:C
.∀x:C
.∀u:T
.clear (CHead e (Bind b) u) x
→eq C x (CHead e (Bind b) u)