DEFINITION cimp_bind()
TYPE =
∀c1:C
.∀c2:C
.cimp c1 c2
→∀b:B.∀v:T.(cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v))
BODY =
assume c1: C
assume c2: C
we must prove
cimp c1 c2
→∀b:B.∀v:T.(cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v))
or equivalently
∀b:B
.∀d1:C
.∀w:T
.∀h:nat
.getl h c1 (CHead d1 (Bind b) w)
→ex C λd2:C.getl h c2 (CHead d2 (Bind b) w)
→∀b:B.∀v:T.(cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v))
suppose H:
∀b:B
.∀d1:C
.∀w:T
.∀h:nat
.getl h c1 (CHead d1 (Bind b) w)
→ex C λd2:C.getl h c2 (CHead d2 (Bind b) w)
assume b: B
assume v: T
we must prove cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v)
or equivalently
∀b0:B
.∀d1:C
.∀w:T
.∀h:nat
.getl h (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)
→ex C λd2:C.getl h (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
assume b0: B
assume d1: C
assume w: T
assume h: nat
suppose H0: getl h (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)
suppose H1: getl O (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)
(H2)
by (getl_gen_O . . H1)
we proved clear (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead d1 (Bind b0) w) (CHead c1 (Bind b) v)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind b0) w OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead c1 (Bind b) v OF CSort ⇒d1 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead d1 (Bind b0) w)
λe:C.<λ:C.C> CASE e OF CSort ⇒d1 | CHead c ⇒c (CHead c1 (Bind b) v)
end of H2
(h1)
(H3)
by (getl_gen_O . . H1)
we proved clear (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead d1 (Bind b0) w) (CHead c1 (Bind b) v)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind b0) w OF
CSort ⇒b0
| CHead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
<λ:C.B>
CASE CHead c1 (Bind b) v OF
CSort ⇒b0
| CHead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
eq
B
λe:C.<λ:C.B> CASE e OF CSort ⇒b0 | CHead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
CHead d1 (Bind b0) w
λe:C.<λ:C.B> CASE e OF CSort ⇒b0 | CHead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
CHead c1 (Bind b) v
end of H3
(h1)
(H4)
by (getl_gen_O . . H1)
we proved clear (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead d1 (Bind b0) w) (CHead c1 (Bind b) v)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d1 (Bind b0) w OF CSort ⇒w | CHead t⇒t
<λ:C.T> CASE CHead c1 (Bind b) v OF CSort ⇒w | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒w | CHead t⇒t (CHead d1 (Bind b0) w)
λe:C.<λ:C.T> CASE e OF CSort ⇒w | CHead t⇒t (CHead c1 (Bind b) v)
end of H4
suppose H5: eq B b0 b
suppose : eq C d1 c1
(h1)
by (getl_refl . . .)
we proved getl O (CHead c2 (Bind b) v) (CHead c2 (Bind b) v)
by (ex_intro . . . previous)
we proved ex C λd2:C.getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b) v)
by (eq_ind_r . . . previous . H5)
ex C λd2:C.getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b0) v)
end of h1
(h2)
consider H4
we proved
eq
T
<λ:C.T> CASE CHead d1 (Bind b0) w OF CSort ⇒w | CHead t⇒t
<λ:C.T> CASE CHead c1 (Bind b) v OF CSort ⇒w | CHead t⇒t
eq T w v
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex C λd2:C.getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
eq B b0 b
→(eq C d1 c1
→ex C λd2:C.getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w))
end of h1
(h2)
consider H3
we proved
eq
B
<λ:C.B>
CASE CHead d1 (Bind b0) w OF
CSort ⇒b0
| CHead k ⇒<λ:K.B> CASE k OF Bind b1⇒b1 | Flat ⇒b0
<λ:C.B>
CASE CHead c1 (Bind b) v 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 d1 c1
→ex C λd2:C.getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
end of h1
(h2)
consider H2
we proved
eq
C
<λ:C.C> CASE CHead d1 (Bind b0) w OF CSort ⇒d1 | CHead c ⇒c
<λ:C.C> CASE CHead c1 (Bind b) v OF CSort ⇒d1 | CHead c ⇒c
eq C d1 c1
end of h2
by (h1 h2)
we proved ex C λd2:C.getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
getl O (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)
→ex C λd2:C.getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
assume h0: nat
suppose :
getl h0 (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)
→ex C λd2:C.getl h0 (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
suppose H1: getl (S h0) (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)
(H_x)
by (getl_gen_S . . . . . H1)
we proved getl (r (Bind b) h0) c1 (CHead d1 (Bind b0) w)
by (H . . . . previous)
ex C λd2:C.getl (r (Bind b) h0) c2 (CHead d2 (Bind b0) w)
end of H_x
(H2) consider H_x
consider H2
we proved ex C λd2:C.getl (r (Bind b) h0) c2 (CHead d2 (Bind b0) w)
that is equivalent to ex C λd2:C.getl h0 c2 (CHead d2 (Bind b0) w)
we proceed by induction on the previous result to prove ex C λd2:C.getl (S h0) (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
case ex_intro : x:C H3:getl h0 c2 (CHead x (Bind b0) w) ⇒
the thesis becomes ex C λd2:C.getl (S h0) (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
consider H3
we proved getl h0 c2 (CHead x (Bind b0) w)
that is equivalent to getl (r (Bind b) h0) c2 (CHead x (Bind b0) w)
by (getl_head . . . . previous .)
we proved getl (S h0) (CHead c2 (Bind b) v) (CHead x (Bind b0) w)
by (ex_intro . . . previous)
ex C λd2:C.getl (S h0) (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
we proved ex C λd2:C.getl (S h0) (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
∀H1:getl (S h0) (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)
.ex C λd2:C.getl (S h0) (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
by (previous . H0)
we proved ex C λd2:C.getl h (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
we proved
∀b0:B
.∀d1:C
.∀w:T
.∀h:nat
.getl h (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)
→ex C λd2:C.getl h (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)
that is equivalent to cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v)
we proved
∀b:B
.∀d1:C
.∀w:T
.∀h:nat
.getl h c1 (CHead d1 (Bind b) w)
→ex C λd2:C.getl h c2 (CHead d2 (Bind b) w)
→∀b:B.∀v:T.(cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v))
that is equivalent to
cimp c1 c2
→∀b:B.∀v:T.(cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v))
we proved
∀c1:C
.∀c2:C
.cimp c1 c2
→∀b:B.∀v:T.(cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v))