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