DEFINITION wf3_gen_bind1()
TYPE =
∀g:G
.∀c1:C
.∀x:C
.∀v:T
.∀b:B
.wf3 g (CHead c1 (Bind b) v) x
→(or
ex3_2 C T λc2:C.λ:T.eq C x (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g c1 c2 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc2:C.eq C x (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c1 c2
λ:C.∀w:T.(ty3 g c1 v w)→False)
BODY =
assume g: G
assume c1: C
assume x: C
assume v: T
assume b: B
suppose H: wf3 g (CHead c1 (Bind b) v) x
assume y: C
suppose H0: wf3 g y x
we proceed by induction on H0 to prove
eq C y (CHead c1 (Bind b) v)
→(or
ex3_2 C T λc2:C.λ:T.eq C x (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g c1 c2 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc2:C.eq C x (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c1 c2
λ:C.∀w:T.(ty3 g c1 v w)→False)
case wf3_sort : m:nat ⇒
the thesis becomes
∀H1:eq C (CSort m) (CHead c1 (Bind b) v)
.or
ex3_2 C T λc2:C.λ:T.eq C (CSort m) (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g c1 c2 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc2:C.eq C (CSort m) (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c1 c2
λ:C.∀w:T.(ty3 g c1 v w)→False
suppose H1: eq C (CSort m) (CHead c1 (Bind b) v)
(H2)
we proceed by induction on H1 to prove <λ:C.Prop> CASE CHead c1 (Bind b) v OF CSort ⇒True | CHead ⇒False
case refl_equal : ⇒
the thesis becomes <λ:C.Prop> CASE CSort m OF CSort ⇒True | CHead ⇒False
consider I
we proved True
<λ:C.Prop> CASE CSort m OF CSort ⇒True | CHead ⇒False
<λ:C.Prop> CASE CHead c1 (Bind b) v OF CSort ⇒True | CHead ⇒False
end of H2
consider H2
we proved <λ:C.Prop> CASE CHead c1 (Bind b) v OF CSort ⇒True | CHead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or
ex3_2 C T λc2:C.λ:T.eq C (CSort m) (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g c1 c2 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc2:C.eq C (CSort m) (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c1 c2
λ:C.∀w:T.(ty3 g c1 v w)→False
we proved
or
ex3_2 C T λc2:C.λ:T.eq C (CSort m) (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g c1 c2 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc2:C.eq C (CSort m) (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c1 c2
λ:C.∀w:T.(ty3 g c1 v w)→False
∀H1:eq C (CSort m) (CHead c1 (Bind b) v)
.or
ex3_2 C T λc2:C.λ:T.eq C (CSort m) (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g c1 c2 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc2:C.eq C (CSort m) (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c1 c2
λ:C.∀w:T.(ty3 g c1 v w)→False
case wf3_bind : c0:C c2:C H1:wf3 g c0 c2 u:T t:T H3:ty3 g c0 u t b0:B ⇒
the thesis becomes
∀H4:eq C (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v)
.or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
(H2) by induction hypothesis we know
eq C c0 (CHead c1 (Bind b) v)
→(or
ex3_2 C T λc3:C.λ:T.eq C c2 (CHead c3 (Bind b) v) λc3:C.λ:T.wf3 g c1 c3 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C c2 (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False)
suppose H4: eq C (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v)
(H5)
by (f_equal . . . . . H4)
we proved
eq
C
<λ:C.C> CASE CHead c0 (Bind b0) u OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 (Bind b) v OF CSort ⇒c0 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c0 (Bind b0) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c1 (Bind b) v)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
B
<λ:C.B>
CASE CHead c0 (Bind b0) u 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 c0 (Bind b0) u
λ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 H6
(h1)
(H7)
by (f_equal . . . . . H4)
we proved
eq
T
<λ:C.T> CASE CHead c0 (Bind b0) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead c1 (Bind b) v OF CSort ⇒u | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead c0 (Bind b0) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead c1 (Bind b) v)
end of H7
suppose H8: eq B b0 b
suppose H9: eq C c0 c1
(H10)
consider H7
we proved
eq
T
<λ:C.T> CASE CHead c0 (Bind b0) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead c1 (Bind b) v OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u v
we proceed by induction on the previous result to prove ty3 g c0 v t
case refl_equal : ⇒
the thesis becomes the hypothesis H3
ty3 g c0 v t
end of H10
(h1)
(H11)
we proceed by induction on H9 to prove ty3 g c1 v t
case refl_equal : ⇒
the thesis becomes the hypothesis H10
ty3 g c1 v t
end of H11
(H13)
we proceed by induction on H9 to prove wf3 g c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
wf3 g c1 c2
end of H13
by (refl_equal . .)
we proved eq C (CHead c2 (Bind b) v) (CHead c2 (Bind b) v)
by (ex3_2_intro . . . . . . . previous H13 H11)
we proved
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind b) v) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
by (or_introl . . previous)
or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind b) v) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C (CHead c2 (Bind b) v) (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
end of h1
(h2)
consider H7
we proved
eq
T
<λ:C.T> CASE CHead c0 (Bind b0) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead c1 (Bind b) v OF CSort ⇒u | CHead t0⇒t0
eq T u v
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind b) u) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C (CHead c2 (Bind b) u) (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
by (eq_ind_r . . . previous . H8)
we proved
or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
eq B b0 b
→(eq C c0 c1
→(or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False))
end of h1
(h2)
consider H6
we proved
eq
B
<λ:C.B>
CASE CHead c0 (Bind b0) u 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 c0 c1
→(or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False)
end of h1
(h2)
consider H5
we proved
eq
C
<λ:C.C> CASE CHead c0 (Bind b0) u OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 (Bind b) v OF CSort ⇒c0 | CHead c ⇒c
eq C c0 c1
end of h2
by (h1 h2)
we proved
or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
∀H4:eq C (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v)
.or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C (CHead c2 (Bind b0) u) (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
case wf3_void : c0:C c2:C H1:wf3 g c0 c2 u:T H3:∀t:T.(ty3 g c0 u t)→False b0:B ⇒
the thesis becomes
∀H4:eq C (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v)
.or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind Void) (TSort O)) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C
.eq
C
CHead c2 (Bind Void) (TSort O)
CHead c3 (Bind Void) (TSort O)
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
(H2) by induction hypothesis we know
eq C c0 (CHead c1 (Bind b) v)
→(or
ex3_2 C T λc3:C.λ:T.eq C c2 (CHead c3 (Bind b) v) λc3:C.λ:T.wf3 g c1 c3 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C c2 (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False)
suppose H4: eq C (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v)
(H5)
by (f_equal . . . . . H4)
we proved
eq
C
<λ:C.C> CASE CHead c0 (Bind b0) u OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 (Bind b) v OF CSort ⇒c0 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c0 (Bind b0) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c1 (Bind b) v)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
B
<λ:C.B>
CASE CHead c0 (Bind b0) u 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 c0 (Bind b0) u
λ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 H6
(h1)
(H7)
by (f_equal . . . . . H4)
we proved
eq
T
<λ:C.T> CASE CHead c0 (Bind b0) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead c1 (Bind b) v OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead c0 (Bind b0) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead c1 (Bind b) v)
end of H7
suppose : eq B b0 b
suppose H9: eq C c0 c1
(H10)
consider H7
we proved
eq
T
<λ:C.T> CASE CHead c0 (Bind b0) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead c1 (Bind b) v OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u v
we proceed by induction on the previous result to prove ∀t0:T.(ty3 g c0 v t0)→False
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀t0:T.(ty3 g c0 v t0)→False
end of H10
(H11)
we proceed by induction on H9 to prove ∀t:T.(ty3 g c1 v t)→False
case refl_equal : ⇒
the thesis becomes the hypothesis H10
∀t:T.(ty3 g c1 v t)→False
end of H11
(H13)
we proceed by induction on H9 to prove wf3 g c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
wf3 g c1 c2
end of H13
by (refl_equal . .)
we proved
eq
C
CHead c2 (Bind Void) (TSort O)
CHead c2 (Bind Void) (TSort O)
by (ex3_intro . . . . . previous H13 H11)
we proved
ex3
C
λc3:C
.eq
C
CHead c2 (Bind Void) (TSort O)
CHead c3 (Bind Void) (TSort O)
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
by (or_intror . . previous)
we proved
or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind Void) (TSort O)) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C
.eq
C
CHead c2 (Bind Void) (TSort O)
CHead c3 (Bind Void) (TSort O)
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
eq B b0 b
→(eq C c0 c1
→(or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind Void) (TSort O)) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C
.eq
C
CHead c2 (Bind Void) (TSort O)
CHead c3 (Bind Void) (TSort O)
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False))
end of h1
(h2)
consider H6
we proved
eq
B
<λ:C.B>
CASE CHead c0 (Bind b0) u 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 c0 c1
→(or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind Void) (TSort O)) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C
.eq
C
CHead c2 (Bind Void) (TSort O)
CHead c3 (Bind Void) (TSort O)
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False)
end of h1
(h2)
consider H5
we proved
eq
C
<λ:C.C> CASE CHead c0 (Bind b0) u OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 (Bind b) v OF CSort ⇒c0 | CHead c ⇒c
eq C c0 c1
end of h2
by (h1 h2)
we proved
or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind Void) (TSort O)) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C
.eq
C
CHead c2 (Bind Void) (TSort O)
CHead c3 (Bind Void) (TSort O)
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
∀H4:eq C (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v)
.or
ex3_2
C
T
λc3:C.λ:T.eq C (CHead c2 (Bind Void) (TSort O)) (CHead c3 (Bind b) v)
λc3:C.λ:T.wf3 g c1 c3
λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C
.eq
C
CHead c2 (Bind Void) (TSort O)
CHead c3 (Bind Void) (TSort O)
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
case wf3_flat : c0:C c2:C :wf3 g c0 c2 u:T f:F ⇒
the thesis becomes
∀H3:eq C (CHead c0 (Flat f) u) (CHead c1 (Bind b) v)
.or
ex3_2 C T λc3:C.λ:T.eq C c2 (CHead c3 (Bind b) v) λc3:C.λ:T.wf3 g c1 c3 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C c2 (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
() by induction hypothesis we know
eq C c0 (CHead c1 (Bind b) v)
→(or
ex3_2 C T λc3:C.λ:T.eq C c2 (CHead c3 (Bind b) v) λc3:C.λ:T.wf3 g c1 c3 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C c2 (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False)
suppose H3: eq C (CHead c0 (Flat f) u) (CHead c1 (Bind b) v)
(H4)
we proceed by induction on H3 to prove
<λ:C.Prop>
CASE CHead c1 (Bind b) v OF
CSort ⇒False
| CHead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead c0 (Flat f) u OF
CSort ⇒False
| CHead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:C.Prop>
CASE CHead c0 (Flat f) u OF
CSort ⇒False
| CHead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:C.Prop>
CASE CHead c1 (Bind b) v 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 c1 (Bind b) v 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
or
ex3_2 C T λc3:C.λ:T.eq C c2 (CHead c3 (Bind b) v) λc3:C.λ:T.wf3 g c1 c3 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C c2 (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
we proved
or
ex3_2 C T λc3:C.λ:T.eq C c2 (CHead c3 (Bind b) v) λc3:C.λ:T.wf3 g c1 c3 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C c2 (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
∀H3:eq C (CHead c0 (Flat f) u) (CHead c1 (Bind b) v)
.or
ex3_2 C T λc3:C.λ:T.eq C c2 (CHead c3 (Bind b) v) λc3:C.λ:T.wf3 g c1 c3 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc3:C.eq C c2 (CHead c3 (Bind Void) (TSort O))
λc3:C.wf3 g c1 c3
λ:C.∀w:T.(ty3 g c1 v w)→False
we proved
eq C y (CHead c1 (Bind b) v)
→(or
ex3_2 C T λc2:C.λ:T.eq C x (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g c1 c2 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc2:C.eq C x (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c1 c2
λ:C.∀w:T.(ty3 g c1 v w)→False)
we proved
∀y:C
.wf3 g y x
→(eq C y (CHead c1 (Bind b) v)
→(or
ex3_2 C T λc2:C.λ:T.eq C x (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g c1 c2 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc2:C.eq C x (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c1 c2
λ:C.∀w:T.(ty3 g c1 v w)→False))
by (insert_eq . . . . previous H)
we proved
or
ex3_2 C T λc2:C.λ:T.eq C x (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g c1 c2 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc2:C.eq C x (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c1 c2
λ:C.∀w:T.(ty3 g c1 v w)→False
we proved
∀g:G
.∀c1:C
.∀x:C
.∀v:T
.∀b:B
.wf3 g (CHead c1 (Bind b) v) x
→(or
ex3_2 C T λc2:C.λ:T.eq C x (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g c1 c2 λ:C.λw:T.ty3 g c1 v w
ex3
C
λc2:C.eq C x (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c1 c2
λ:C.∀w:T.(ty3 g c1 v w)→False)