DEFINITION csubc_gen_head_l()
TYPE =
∀g:G
.∀c1:C
.∀x:C
.∀v:T
.∀k:K
.csubc g (CHead c1 k v) x
→(or3
ex2 C λc2:C.eq C x (CHead c2 k v) λc2:C.csubc g c1 c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C x (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g c1 c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C x (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g c1 c2)
BODY =
assume g: G
assume c1: C
assume x: C
assume v: T
assume k: K
suppose H: csubc g (CHead c1 k v) x
assume y: C
suppose H0: csubc g y x
we proceed by induction on H0 to prove
eq C y (CHead c1 k v)
→(or3
ex2 C λc2:C.eq C x (CHead c2 k v) λc2:C.csubc g c1 c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C x (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g c1 c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C x (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g c1 c2)
case csubc_sort : n:nat ⇒
the thesis becomes
∀H1:eq C (CSort n) (CHead c1 k v)
.or3
ex2 C λc2:C.eq C (CSort n) (CHead c2 k v) λc2:C.csubc g c1 c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C (CSort n) (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g c1 c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C (CSort n) (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g c1 c2
suppose H1: eq C (CSort n) (CHead c1 k v)
(H2)
we proceed by induction on H1 to prove <λ:C.Prop> CASE CHead c1 k v 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 c1 k v OF CSort ⇒True | CHead ⇒False
end of H2
consider H2
we proved <λ:C.Prop> CASE CHead c1 k v OF CSort ⇒True | CHead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or3
ex2 C λc2:C.eq C (CSort n) (CHead c2 k v) λc2:C.csubc g c1 c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C (CSort n) (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g c1 c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C (CSort n) (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g c1 c2
we proved
or3
ex2 C λc2:C.eq C (CSort n) (CHead c2 k v) λc2:C.csubc g c1 c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C (CSort n) (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g c1 c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C (CSort n) (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g c1 c2
∀H1:eq C (CSort n) (CHead c1 k v)
.or3
ex2 C λc2:C.eq C (CSort n) (CHead c2 k v) λc2:C.csubc g c1 c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C (CSort n) (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g c1 c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C (CSort n) (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g c1 c2
case csubc_head : c0:C c2:C H1:csubc g c0 c2 k0:K v0:T ⇒
the thesis becomes
∀H3:eq C (CHead c0 k0 v0) (CHead c1 k v)
.or3
ex2 C λc3:C.eq C (CHead c2 k0 v0) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 k0 v0) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 k0 v0) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
(H2) by induction hypothesis we know
eq C c0 (CHead c1 k v)
→(or3
ex2 C λc3:C.eq C c2 (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C c2 (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C c2 (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3)
suppose H3: eq C (CHead c0 k0 v0) (CHead c1 k v)
(H4)
by (f_equal . . . . . H3)
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 v0 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k v OF CSort ⇒c0 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c0 k0 v0)
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c1 k v)
end of H4
(h1)
(H5)
by (f_equal . . . . . H3)
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 v0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c1 k v OF CSort ⇒k0 | CHead k1 ⇒k1
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c0 k0 v0)
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c1 k v)
end of H5
(h1)
(H6)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:C.T> CASE CHead c0 k0 v0 OF CSort ⇒v0 | CHead t⇒t
<λ:C.T> CASE CHead c1 k v OF CSort ⇒v0 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒v0 | CHead t⇒t (CHead c0 k0 v0)
λe:C.<λ:C.T> CASE e OF CSort ⇒v0 | CHead t⇒t (CHead c1 k v)
end of H6
suppose H7: eq K k0 k
suppose H8: eq C c0 c1
(h1)
(H10)
we proceed by induction on H8 to prove csubc g c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
csubc g c1 c2
end of H10
by (refl_equal . .)
we proved eq C (CHead c2 k v) (CHead c2 k v)
by (ex_intro2 . . . . previous H10)
we proved ex2 C λc3:C.eq C (CHead c2 k v) (CHead c3 k v) λc3:C.csubc g c1 c3
by (or3_intro0 . . . previous)
we proved
or3
ex2 C λc3:C.eq C (CHead c2 k v) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 k v) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 k v) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
by (eq_ind_r . . . previous . H7)
or3
ex2 C λc3:C.eq C (CHead c2 k0 v) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 k0 v) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 k0 v) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
end of h1
(h2)
consider H6
we proved
eq
T
<λ:C.T> CASE CHead c0 k0 v0 OF CSort ⇒v0 | CHead t⇒t
<λ:C.T> CASE CHead c1 k v OF CSort ⇒v0 | CHead t⇒t
eq T v0 v
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or3
ex2 C λc3:C.eq C (CHead c2 k0 v0) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 k0 v0) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 k0 v0) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
eq K k0 k
→(eq C c0 c1
→(or3
ex2 C λc3:C.eq C (CHead c2 k0 v0) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 k0 v0) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 k0 v0) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3))
end of h1
(h2)
consider H5
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 v0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c1 k v OF CSort ⇒k0 | CHead k1 ⇒k1
eq K k0 k
end of h2
by (h1 h2)
eq C c0 c1
→(or3
ex2 C λc3:C.eq C (CHead c2 k0 v0) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 k0 v0) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 k0 v0) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3)
end of h1
(h2)
consider H4
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 v0 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k v OF CSort ⇒c0 | CHead c ⇒c
eq C c0 c1
end of h2
by (h1 h2)
we proved
or3
ex2 C λc3:C.eq C (CHead c2 k0 v0) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 k0 v0) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 k0 v0) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
∀H3:eq C (CHead c0 k0 v0) (CHead c1 k v)
.or3
ex2 C λc3:C.eq C (CHead c2 k0 v0) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 k0 v0) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 k0 v0) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
case csubc_void : c0:C c2:C H1:csubc g c0 c2 b:B H3:not (eq B b Void) u1:T u2:T ⇒
the thesis becomes
∀H4:eq C (CHead c0 (Bind Void) u1) (CHead c1 k v)
.or3
ex2 C λc3:C.eq C (CHead c2 (Bind b) u2) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb0:B.λc3:C.λv2:T.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind b0) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb0:B.λ:C.λ:T.not (eq B b0 Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
(H2) by induction hypothesis we know
eq C c0 (CHead c1 k v)
→(or3
ex2 C λc3:C.eq C c2 (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C c2 (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C c2 (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3)
suppose H4: eq C (CHead c0 (Bind Void) u1) (CHead c1 k v)
(H5)
by (f_equal . . . . . H4)
we proved
eq
C
<λ:C.C> CASE CHead c0 (Bind Void) u1 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k v OF CSort ⇒c0 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c0 (Bind Void) u1)
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c1 k v)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
K
<λ:C.K> CASE CHead c0 (Bind Void) u1 OF CSort ⇒Bind Void | CHead k0 ⇒k0
<λ:C.K> CASE CHead c1 k v OF CSort ⇒Bind Void | CHead k0 ⇒k0
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒Bind Void | CHead k0 ⇒k0
CHead c0 (Bind Void) u1
λe:C.<λ:C.K> CASE e OF CSort ⇒Bind Void | CHead k0 ⇒k0 (CHead c1 k v)
end of H6
(H8)
consider H6
we proved
eq
K
<λ:C.K> CASE CHead c0 (Bind Void) u1 OF CSort ⇒Bind Void | CHead k0 ⇒k0
<λ:C.K> CASE CHead c1 k v OF CSort ⇒Bind Void | CHead k0 ⇒k0
eq K (Bind Void) k
end of H8
suppose H9: eq C c0 c1
(H10)
we proceed by induction on H9 to prove
eq C c1 (CHead c1 k v)
→(or3
ex2 C λc3:C.eq C c2 (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C c2 (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb0:B.λc3:C.λv2:T.eq C c2 (CHead c3 (Bind b0) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb0:B.λ:C.λ:T.not (eq B b0 Void)
λ:B.λc3:C.λ:T.csubc g c1 c3)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
eq C c1 (CHead c1 k v)
→(or3
ex2 C λc3:C.eq C c2 (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C c2 (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb0:B.λc3:C.λv2:T.eq C c2 (CHead c3 (Bind b0) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb0:B.λ:C.λ:T.not (eq B b0 Void)
λ:B.λc3:C.λ:T.csubc g c1 c3)
end of H10
(H11)
we proceed by induction on H9 to prove csubc g c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
csubc g c1 c2
end of H11
we proceed by induction on H8 to prove
or3
ex2 C λc3:C.eq C (CHead c2 (Bind b) u2) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb0:B.λc3:C.λv2:T.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind b0) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb0:B.λ:C.λ:T.not (eq B b0 Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
case refl_equal : ⇒
the thesis becomes
or3
ex2
C
λc3:C.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind Void) v)
λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K (Bind Void) (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb0:B.λc3:C.λv2:T.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind b0) v2)
λ:B.λ:C.λ:T.eq K (Bind Void) (Bind Void)
λb0:B.λ:C.λ:T.not (eq B b0 Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
(h1)
by (refl_equal . .)
eq C (CHead c2 (Bind b) u2) (CHead c2 (Bind b) u2)
end of h1
(h2)
by (refl_equal . .)
eq K (Bind Void) (Bind Void)
end of h2
by (ex4_3_intro . . . . . . . . . . h1 h2 H3 H11)
we proved
ex4_3
B
C
T
λb0:B.λc3:C.λv2:T.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind b0) v2)
λ:B.λ:C.λ:T.eq K (Bind Void) (Bind Void)
λb0:B.λ:C.λ:T.not (eq B b0 Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
by (or3_intro2 . . . previous)
or3
ex2
C
λc3:C.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind Void) v)
λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K (Bind Void) (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb0:B.λc3:C.λv2:T.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind b0) v2)
λ:B.λ:C.λ:T.eq K (Bind Void) (Bind Void)
λb0:B.λ:C.λ:T.not (eq B b0 Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
we proved
or3
ex2 C λc3:C.eq C (CHead c2 (Bind b) u2) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb0:B.λc3:C.λv2:T.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind b0) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb0:B.λ:C.λ:T.not (eq B b0 Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
eq C c0 c1
→(or3
ex2 C λc3:C.eq C (CHead c2 (Bind b) u2) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb0:B.λc3:C.λv2:T.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind b0) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb0:B.λ:C.λ:T.not (eq B b0 Void)
λ:B.λc3:C.λ:T.csubc g c1 c3)
end of h1
(h2)
consider H5
we proved
eq
C
<λ:C.C> CASE CHead c0 (Bind Void) u1 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k v OF CSort ⇒c0 | CHead c ⇒c
eq C c0 c1
end of h2
by (h1 h2)
we proved
or3
ex2 C λc3:C.eq C (CHead c2 (Bind b) u2) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb0:B.λc3:C.λv2:T.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind b0) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb0:B.λ:C.λ:T.not (eq B b0 Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
∀H4:eq C (CHead c0 (Bind Void) u1) (CHead c1 k v)
.or3
ex2 C λc3:C.eq C (CHead c2 (Bind b) u2) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb0:B.λc3:C.λv2:T.eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind b0) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb0:B.λ:C.λ:T.not (eq B b0 Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
case csubc_abst : c0:C c2:C H1:csubc g c0 c2 v0:T a:A H3:sc3 g (asucc g a) c0 v0 w:T H4:sc3 g a c2 w ⇒
the thesis becomes
∀H5:eq C (CHead c0 (Bind Abst) v0) (CHead c1 k v)
.or3
ex2 C λc3:C.eq C (CHead c2 (Bind Abbr) w) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw0:T.λ:A.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
(H2) by induction hypothesis we know
eq C c0 (CHead c1 k v)
→(or3
ex2 C λc3:C.eq C c2 (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw:T.λ:A.eq C c2 (CHead c3 (Bind Abbr) w)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc3:C.λw:T.λa:A.sc3 g a c3 w
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C c2 (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3)
suppose H5: eq C (CHead c0 (Bind Abst) v0) (CHead c1 k v)
(H6)
by (f_equal . . . . . H5)
we proved
eq
C
<λ:C.C> CASE CHead c0 (Bind Abst) v0 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k v OF CSort ⇒c0 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c0 (Bind Abst) v0)
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c1 k v)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
K
<λ:C.K> CASE CHead c0 (Bind Abst) v0 OF CSort ⇒Bind Abst | CHead k0 ⇒k0
<λ:C.K> CASE CHead c1 k v OF CSort ⇒Bind Abst | CHead k0 ⇒k0
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒Bind Abst | CHead k0 ⇒k0
CHead c0 (Bind Abst) v0
λe:C.<λ:C.K> CASE e OF CSort ⇒Bind Abst | CHead k0 ⇒k0 (CHead c1 k v)
end of H7
(h1)
(H8)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:C.T> CASE CHead c0 (Bind Abst) v0 OF CSort ⇒v0 | CHead t⇒t
<λ:C.T> CASE CHead c1 k v OF CSort ⇒v0 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒v0 | CHead t⇒t (CHead c0 (Bind Abst) v0)
λe:C.<λ:C.T> CASE e OF CSort ⇒v0 | CHead t⇒t (CHead c1 k v)
end of H8
suppose H9: eq K (Bind Abst) k
suppose H10: eq C c0 c1
(H11)
consider H8
we proved
eq
T
<λ:C.T> CASE CHead c0 (Bind Abst) v0 OF CSort ⇒v0 | CHead t⇒t
<λ:C.T> CASE CHead c1 k v OF CSort ⇒v0 | CHead t⇒t
that is equivalent to eq T v0 v
we proceed by induction on the previous result to prove sc3 g (asucc g a) c0 v
case refl_equal : ⇒
the thesis becomes the hypothesis H3
sc3 g (asucc g a) c0 v
end of H11
(H12)
we proceed by induction on H10 to prove sc3 g (asucc g a) c1 v
case refl_equal : ⇒
the thesis becomes the hypothesis H11
sc3 g (asucc g a) c1 v
end of H12
(H13)
we proceed by induction on H10 to prove
eq C c1 (CHead c1 k v)
→(or3
ex2 C λc3:C.eq C c2 (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw0:T.λ:A.eq C c2 (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C c2 (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
eq C c1 (CHead c1 k v)
→(or3
ex2 C λc3:C.eq C c2 (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw0:T.λ:A.eq C c2 (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C c2 (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3)
end of H13
(H14)
we proceed by induction on H10 to prove csubc g c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
csubc g c1 c2
end of H14
we proceed by induction on H9 to prove
or3
ex2 C λc3:C.eq C (CHead c2 (Bind Abbr) w) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw0:T.λ:A.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
case refl_equal : ⇒
the thesis becomes
or3
ex2
C
λc3:C.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abst) v)
λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K (Bind Abst) (Bind Abst)
λc3:C.λw0:T.λ:A.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K (Bind Abst) (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
(h1)
by (refl_equal . .)
eq K (Bind Abst) (Bind Abst)
end of h1
(h2)
by (refl_equal . .)
eq C (CHead c2 (Bind Abbr) w) (CHead c2 (Bind Abbr) w)
end of h2
by (ex5_3_intro . . . . . . . . . . . h1 h2 H14 H12 H4)
we proved
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K (Bind Abst) (Bind Abst)
λc3:C.λw0:T.λ:A.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
by (or3_intro1 . . . previous)
or3
ex2
C
λc3:C.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abst) v)
λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K (Bind Abst) (Bind Abst)
λc3:C.λw0:T.λ:A.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K (Bind Abst) (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
we proved
or3
ex2 C λc3:C.eq C (CHead c2 (Bind Abbr) w) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw0:T.λ:A.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
eq K (Bind Abst) k
→(eq C c0 c1
→(or3
ex2 C λc3:C.eq C (CHead c2 (Bind Abbr) w) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw0:T.λ:A.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3))
end of h1
(h2)
consider H7
we proved
eq
K
<λ:C.K> CASE CHead c0 (Bind Abst) v0 OF CSort ⇒Bind Abst | CHead k0 ⇒k0
<λ:C.K> CASE CHead c1 k v OF CSort ⇒Bind Abst | CHead k0 ⇒k0
eq K (Bind Abst) k
end of h2
by (h1 h2)
eq C c0 c1
→(or3
ex2 C λc3:C.eq C (CHead c2 (Bind Abbr) w) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw0:T.λ:A.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3)
end of h1
(h2)
consider H6
we proved
eq
C
<λ:C.C> CASE CHead c0 (Bind Abst) v0 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k v OF CSort ⇒c0 | CHead c ⇒c
eq C c0 c1
end of h2
by (h1 h2)
we proved
or3
ex2 C λc3:C.eq C (CHead c2 (Bind Abbr) w) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw0:T.λ:A.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
∀H5:eq C (CHead c0 (Bind Abst) v0) (CHead c1 k v)
.or3
ex2 C λc3:C.eq C (CHead c2 (Bind Abbr) w) (CHead c3 k v) λc3:C.csubc g c1 c3
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc3:C.λw0:T.λ:A.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr) w0)
λc3:C.λ:T.λ:A.csubc g c1 c3
λ:C.λ:T.λa0:A.sc3 g (asucc g a0) c1 v
λc3:C.λw0:T.λa0:A.sc3 g a0 c3 w0
ex4_3
B
C
T
λb:B.λc3:C.λv2:T.eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc3:C.λ:T.csubc g c1 c3
we proved
eq C y (CHead c1 k v)
→(or3
ex2 C λc2:C.eq C x (CHead c2 k v) λc2:C.csubc g c1 c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C x (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g c1 c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C x (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g c1 c2)
we proved
∀y:C
.csubc g y x
→(eq C y (CHead c1 k v)
→(or3
ex2 C λc2:C.eq C x (CHead c2 k v) λc2:C.csubc g c1 c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C x (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g c1 c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C x (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g c1 c2))
by (insert_eq . . . . previous H)
we proved
or3
ex2 C λc2:C.eq C x (CHead c2 k v) λc2:C.csubc g c1 c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C x (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g c1 c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C x (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g c1 c2
we proved
∀g:G
.∀c1:C
.∀x:C
.∀v:T
.∀k:K
.csubc g (CHead c1 k v) x
→(or3
ex2 C λc2:C.eq C x (CHead c2 k v) λc2:C.csubc g c1 c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C x (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g c1 c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C x (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g c1 c2)