DEFINITION csubt_gen_abst()
TYPE =
∀g:G
.∀e1:C
.∀c2:C
.∀v1:T
.csubt g (CHead e1 (Bind Abst) v1) c2
→(or
ex2 C λe2:C.eq C c2 (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2 C T λe2:C.λv2:T.eq C c2 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g e1 e2 λ:C.λv2:T.ty3 g e1 v2 v1 λe2:C.λv2:T.ty3 g e2 v2 v1)
BODY =
assume g: G
assume e1: C
assume c2: C
assume v1: T
suppose H: csubt g (CHead e1 (Bind Abst) v1) c2
assume y: C
suppose H0: csubt g y c2
we proceed by induction on H0 to prove
eq C y (CHead e1 (Bind Abst) v1)
→(or
ex2 C λe2:C.eq C c2 (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2 C T λe2:C.λv2:T.eq C c2 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g e1 e2 λ:C.λv2:T.ty3 g e1 v2 v1 λe2:C.λv2:T.ty3 g e2 v2 v1)
case csubt_sort : n:nat ⇒
the thesis becomes
∀H1:eq C (CSort n) (CHead e1 (Bind Abst) v1)
.or
ex2 C λe2:C.eq C (CSort n) (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CSort n) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
suppose H1: eq C (CSort n) (CHead e1 (Bind Abst) v1)
(H2)
we proceed by induction on H1 to prove
<λ:C.Prop>
CASE CHead e1 (Bind Abst) v1 OF
CSort ⇒True
| CHead ⇒False
case refl_equal : ⇒
the thesis becomes <λ:C.Prop> CASE CSort n OF CSort ⇒True | CHead ⇒False
consider I
we proved True
<λ:C.Prop> CASE CSort n OF CSort ⇒True | CHead ⇒False
<λ:C.Prop>
CASE CHead e1 (Bind Abst) v1 OF
CSort ⇒True
| CHead ⇒False
end of H2
consider H2
we proved
<λ:C.Prop>
CASE CHead e1 (Bind Abst) v1 OF
CSort ⇒True
| CHead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or
ex2 C λe2:C.eq C (CSort n) (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CSort n) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
we proved
or
ex2 C λe2:C.eq C (CSort n) (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CSort n) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
∀H1:eq C (CSort n) (CHead e1 (Bind Abst) v1)
.or
ex2 C λe2:C.eq C (CSort n) (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CSort n) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
case csubt_head : c1:C c3:C H1:csubt g c1 c3 k:K u:T ⇒
the thesis becomes
∀H3:eq C (CHead c1 k u) (CHead e1 (Bind Abst) v1)
.or
ex2 C λe2:C.eq C (CHead c3 k u) (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 k u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
(H2) by induction hypothesis we know
eq C c1 (CHead e1 (Bind Abst) v1)
→(or
ex2 C λe2:C.eq C c3 (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2 C T λe2:C.λv2:T.eq C c3 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g e1 e2 λ:C.λv2:T.ty3 g e1 v2 v1 λe2:C.λv2:T.ty3 g e2 v2 v1)
suppose H3: eq C (CHead c1 k u) (CHead e1 (Bind Abst) v1)
(H4)
by (f_equal . . . . . H3)
we proved
eq
C
<λ:C.C> CASE CHead c1 k u OF CSort ⇒c1 | CHead c ⇒c
<λ:C.C> CASE CHead e1 (Bind Abst) v1 OF CSort ⇒c1 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c1 | CHead c ⇒c (CHead c1 k u)
λe:C.<λ:C.C> CASE e OF CSort ⇒c1 | CHead c ⇒c (CHead e1 (Bind Abst) v1)
end of H4
(h1)
(H5)
by (f_equal . . . . . H3)
we proved
eq
K
<λ:C.K> CASE CHead c1 k u OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead e1 (Bind Abst) v1 OF CSort ⇒k | CHead k0 ⇒k0
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k0 ⇒k0 (CHead c1 k u)
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k0 ⇒k0 (CHead e1 (Bind Abst) v1)
end of H5
(h1)
(H6)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:C.T> CASE CHead c1 k u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead e1 (Bind Abst) v1 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead c1 k u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead e1 (Bind Abst) v1)
end of H6
suppose H7: eq K k (Bind Abst)
suppose H8: eq C c1 e1
(h1)
(H10)
we proceed by induction on H8 to prove csubt g e1 c3
case refl_equal : ⇒
the thesis becomes the hypothesis H1
csubt g e1 c3
end of H10
by (refl_equal . .)
we proved eq C (CHead c3 (Bind Abst) v1) (CHead c3 (Bind Abst) v1)
by (ex_intro2 . . . . previous H10)
we proved
ex2
C
λe2:C.eq C (CHead c3 (Bind Abst) v1) (CHead e2 (Bind Abst) v1)
λe2:C.csubt g e1 e2
by (or_introl . . previous)
we proved
or
ex2
C
λe2:C.eq C (CHead c3 (Bind Abst) v1) (CHead e2 (Bind Abst) v1)
λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 (Bind Abst) v1) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
by (eq_ind_r . . . previous . H7)
or
ex2 C λe2:C.eq C (CHead c3 k v1) (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 k v1) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
end of h1
(h2)
consider H6
we proved
eq
T
<λ:C.T> CASE CHead c1 k u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead e1 (Bind Abst) v1 OF CSort ⇒u | CHead t⇒t
eq T u v1
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
ex2 C λe2:C.eq C (CHead c3 k u) (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 k u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
eq K k (Bind Abst)
→(eq C c1 e1
→(or
ex2 C λe2:C.eq C (CHead c3 k u) (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 k u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1))
end of h1
(h2)
consider H5
we proved
eq
K
<λ:C.K> CASE CHead c1 k u OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead e1 (Bind Abst) v1 OF CSort ⇒k | CHead k0 ⇒k0
eq K k (Bind Abst)
end of h2
by (h1 h2)
eq C c1 e1
→(or
ex2 C λe2:C.eq C (CHead c3 k u) (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 k u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1)
end of h1
(h2)
consider H4
we proved
eq
C
<λ:C.C> CASE CHead c1 k u OF CSort ⇒c1 | CHead c ⇒c
<λ:C.C> CASE CHead e1 (Bind Abst) v1 OF CSort ⇒c1 | CHead c ⇒c
eq C c1 e1
end of h2
by (h1 h2)
we proved
or
ex2 C λe2:C.eq C (CHead c3 k u) (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 k u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
∀H3:eq C (CHead c1 k u) (CHead e1 (Bind Abst) v1)
.or
ex2 C λe2:C.eq C (CHead c3 k u) (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 k u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
case csubt_void : c1:C c3:C :csubt g c1 c3 b:B :not (eq B b Void) u1:T u2:T ⇒
the thesis becomes
∀H4:eq C (CHead c1 (Bind Void) u1) (CHead e1 (Bind Abst) v1)
.or
ex2
C
λe2:C.eq C (CHead c3 (Bind b) u2) (CHead e2 (Bind Abst) v1)
λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 (Bind b) u2) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
() by induction hypothesis we know
eq C c1 (CHead e1 (Bind Abst) v1)
→(or
ex2 C λe2:C.eq C c3 (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2 C T λe2:C.λv2:T.eq C c3 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g e1 e2 λ:C.λv2:T.ty3 g e1 v2 v1 λe2:C.λv2:T.ty3 g e2 v2 v1)
suppose H4: eq C (CHead c1 (Bind Void) u1) (CHead e1 (Bind Abst) v1)
(H5)
we proceed by induction on H4 to prove
<λ:C.Prop>
CASE CHead e1 (Bind Abst) v1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead c1 (Bind Void) u1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead c1 (Bind Void) u1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
<λ:C.Prop>
CASE CHead e1 (Bind Abst) v1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
end of H5
consider H5
we proved
<λ:C.Prop>
CASE CHead e1 (Bind Abst) v1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or
ex2
C
λe2:C.eq C (CHead c3 (Bind b) u2) (CHead e2 (Bind Abst) v1)
λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 (Bind b) u2) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
we proved
or
ex2
C
λe2:C.eq C (CHead c3 (Bind b) u2) (CHead e2 (Bind Abst) v1)
λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 (Bind b) u2) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
∀H4:eq C (CHead c1 (Bind Void) u1) (CHead e1 (Bind Abst) v1)
.or
ex2
C
λe2:C.eq C (CHead c3 (Bind b) u2) (CHead e2 (Bind Abst) v1)
λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 (Bind b) u2) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
case csubt_abst : c1:C c3:C H1:csubt g c1 c3 u:T t:T H3:ty3 g c1 u t H4:ty3 g c3 u t ⇒
the thesis becomes
∀H5:eq C (CHead c1 (Bind Abst) t) (CHead e1 (Bind Abst) v1)
.or
ex2
C
λe2:C.eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abst) v1)
λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
(H2) by induction hypothesis we know
eq C c1 (CHead e1 (Bind Abst) v1)
→(or
ex2 C λe2:C.eq C c3 (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2 C T λe2:C.λv2:T.eq C c3 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g e1 e2 λ:C.λv2:T.ty3 g e1 v2 v1 λe2:C.λv2:T.ty3 g e2 v2 v1)
suppose H5: eq C (CHead c1 (Bind Abst) t) (CHead e1 (Bind Abst) v1)
(H6)
by (f_equal . . . . . H5)
we proved
eq
C
<λ:C.C> CASE CHead c1 (Bind Abst) t OF CSort ⇒c1 | CHead c ⇒c
<λ:C.C> CASE CHead e1 (Bind Abst) v1 OF CSort ⇒c1 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c1 | CHead c ⇒c (CHead c1 (Bind Abst) t)
λe:C.<λ:C.C> CASE e OF CSort ⇒c1 | CHead c ⇒c (CHead e1 (Bind Abst) v1)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:C.T> CASE CHead c1 (Bind Abst) t OF CSort ⇒t | CHead t0⇒t0
<λ:C.T> CASE CHead e1 (Bind Abst) v1 OF CSort ⇒t | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒t | CHead t0⇒t0 (CHead c1 (Bind Abst) t)
λe:C.<λ:C.T> CASE e OF CSort ⇒t | CHead t0⇒t0 (CHead e1 (Bind Abst) v1)
end of H7
suppose H8: eq C c1 e1
(H9)
consider H7
we proved
eq
T
<λ:C.T> CASE CHead c1 (Bind Abst) t OF CSort ⇒t | CHead t0⇒t0
<λ:C.T> CASE CHead e1 (Bind Abst) v1 OF CSort ⇒t | CHead t0⇒t0
that is equivalent to eq T t v1
we proceed by induction on the previous result to prove ty3 g c3 u v1
case refl_equal : ⇒
the thesis becomes the hypothesis H4
ty3 g c3 u v1
end of H9
(H10)
consider H7
we proved
eq
T
<λ:C.T> CASE CHead c1 (Bind Abst) t OF CSort ⇒t | CHead t0⇒t0
<λ:C.T> CASE CHead e1 (Bind Abst) v1 OF CSort ⇒t | CHead t0⇒t0
that is equivalent to eq T t v1
we proceed by induction on the previous result to prove ty3 g c1 u v1
case refl_equal : ⇒
the thesis becomes the hypothesis H3
ty3 g c1 u v1
end of H10
(H11)
we proceed by induction on H8 to prove ty3 g e1 u v1
case refl_equal : ⇒
the thesis becomes the hypothesis H10
ty3 g e1 u v1
end of H11
(H13)
we proceed by induction on H8 to prove csubt g e1 c3
case refl_equal : ⇒
the thesis becomes the hypothesis H1
csubt g e1 c3
end of H13
by (refl_equal . .)
we proved eq C (CHead c3 (Bind Abbr) u) (CHead c3 (Bind Abbr) u)
by (ex4_2_intro . . . . . . . . previous H13 H11 H9)
we proved
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
by (or_intror . . previous)
we proved
or
ex2
C
λe2:C.eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abst) v1)
λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
eq C c1 e1
→(or
ex2
C
λe2:C.eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abst) v1)
λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1)
end of h1
(h2)
consider H6
we proved
eq
C
<λ:C.C> CASE CHead c1 (Bind Abst) t OF CSort ⇒c1 | CHead c ⇒c
<λ:C.C> CASE CHead e1 (Bind Abst) v1 OF CSort ⇒c1 | CHead c ⇒c
eq C c1 e1
end of h2
by (h1 h2)
we proved
or
ex2
C
λe2:C.eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abst) v1)
λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
∀H5:eq C (CHead c1 (Bind Abst) t) (CHead e1 (Bind Abst) v1)
.or
ex2
C
λe2:C.eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abst) v1)
λe2:C.csubt g e1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g e1 e2
λ:C.λv2:T.ty3 g e1 v2 v1
λe2:C.λv2:T.ty3 g e2 v2 v1
we proved
eq C y (CHead e1 (Bind Abst) v1)
→(or
ex2 C λe2:C.eq C c2 (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2 C T λe2:C.λv2:T.eq C c2 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g e1 e2 λ:C.λv2:T.ty3 g e1 v2 v1 λe2:C.λv2:T.ty3 g e2 v2 v1)
we proved
∀y:C
.csubt g y c2
→(eq C y (CHead e1 (Bind Abst) v1)
→(or
ex2 C λe2:C.eq C c2 (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2 C T λe2:C.λv2:T.eq C c2 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g e1 e2 λ:C.λv2:T.ty3 g e1 v2 v1 λe2:C.λv2:T.ty3 g e2 v2 v1))
by (insert_eq . . . . previous H)
we proved
or
ex2 C λe2:C.eq C c2 (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2 C T λe2:C.λv2:T.eq C c2 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g e1 e2 λ:C.λv2:T.ty3 g e1 v2 v1 λe2:C.λv2:T.ty3 g e2 v2 v1
we proved
∀g:G
.∀e1:C
.∀c2:C
.∀v1:T
.csubt g (CHead e1 (Bind Abst) v1) c2
→(or
ex2 C λe2:C.eq C c2 (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
ex4_2 C T λe2:C.λv2:T.eq C c2 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g e1 e2 λ:C.λv2:T.ty3 g e1 v2 v1 λe2:C.λv2:T.ty3 g e2 v2 v1)