DEFINITION csuba_gen_abbr_rev()
TYPE =
∀g:G
.∀d1:C
.∀c:C
.∀u1:T
.csuba g c (CHead d1 (Bind Abbr) u1)
→(or3
ex2 C λd2:C.eq C c (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C c (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C c (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
BODY =
assume g: G
assume d1: C
assume c: C
assume u1: T
suppose H: csuba g c (CHead d1 (Bind Abbr) u1)
assume y: C
suppose H0: csuba g c y
we proceed by induction on H0 to prove
eq C y (CHead d1 (Bind Abbr) u1)
→(or3
ex2 C λd2:C.eq C c (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C c (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C c (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
case csuba_sort : n:nat ⇒
the thesis becomes
∀H1:eq C (CSort n) (CHead d1 (Bind Abbr) u1)
.or3
ex2 C λd2:C.eq C (CSort n) (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CSort n) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C (CSort n) (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
suppose H1: eq C (CSort n) (CHead d1 (Bind Abbr) u1)
(H2)
we proceed by induction on H1 to prove
<λ:C.Prop>
CASE CHead d1 (Bind Abbr) u1 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 d1 (Bind Abbr) u1 OF
CSort ⇒True
| CHead ⇒False
end of H2
consider H2
we proved
<λ:C.Prop>
CASE CHead d1 (Bind Abbr) u1 OF
CSort ⇒True
| CHead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or3
ex2 C λd2:C.eq C (CSort n) (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CSort n) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C (CSort n) (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
or3
ex2 C λd2:C.eq C (CSort n) (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CSort n) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C (CSort n) (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
∀H1:eq C (CSort n) (CHead d1 (Bind Abbr) u1)
.or3
ex2 C λd2:C.eq C (CSort n) (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CSort n) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C (CSort n) (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case csuba_head : c1:C c2:C H1:csuba g c1 c2 k:K u:T ⇒
the thesis becomes
∀H3:eq C (CHead c2 k u) (CHead d1 (Bind Abbr) u1)
.or3
ex2 C λd2:C.eq C (CHead c1 k u) (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 k u) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C (CHead c1 k u) (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H2) by induction hypothesis we know
eq C c2 (CHead d1 (Bind Abbr) u1)
→(or3
ex2 C λd2:C.eq C c1 (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C c1 (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C c1 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
suppose H3: eq C (CHead c2 k u) (CHead d1 (Bind Abbr) u1)
(H4)
by (f_equal . . . . . H3)
we proved
eq
C
<λ:C.C> CASE CHead c2 k u OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒c2 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead c2 k u)
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead d1 (Bind Abbr) u1)
end of H4
(h1)
(H5)
by (f_equal . . . . . H3)
we proved
eq
K
<λ:C.K> CASE CHead c2 k u OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒k | CHead k0 ⇒k0
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k0 ⇒k0 (CHead c2 k u)
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k0 ⇒k0 (CHead d1 (Bind Abbr) u1)
end of H5
(h1)
(H6)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:C.T> CASE CHead c2 k u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead c2 k u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d1 (Bind Abbr) u1)
end of H6
suppose H7: eq K k (Bind Abbr)
suppose H8: eq C c2 d1
(h1)
(H10)
we proceed by induction on H8 to prove csuba g c1 d1
case refl_equal : ⇒
the thesis becomes the hypothesis H1
csuba g c1 d1
end of H10
by (refl_equal . .)
we proved eq C (CHead c1 (Bind Abbr) u1) (CHead c1 (Bind Abbr) u1)
by (ex_intro2 . . . . previous H10)
we proved
ex2
C
λd2:C.eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
by (or3_intro0 . . . previous)
we proved
or3
ex2
C
λd2:C.eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2
C
T
λd2:C.λu2:T.eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (eq_ind_r . . . previous . H7)
or3
ex2 C λd2:C.eq C (CHead c1 k u1) (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 k u1) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C (CHead c1 k u1) (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of h1
(h2)
consider H6
we proved
eq
T
<λ:C.T> CASE CHead c2 k u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒u | CHead t⇒t
eq T u u1
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or3
ex2 C λd2:C.eq C (CHead c1 k u) (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 k u) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C (CHead c1 k u) (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
eq K k (Bind Abbr)
→(eq C c2 d1
→(or3
ex2 C λd2:C.eq C (CHead c1 k u) (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 k u) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C (CHead c1 k u) (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1))
end of h1
(h2)
consider H5
we proved
eq
K
<λ:C.K> CASE CHead c2 k u OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒k | CHead k0 ⇒k0
eq K k (Bind Abbr)
end of h2
by (h1 h2)
eq C c2 d1
→(or3
ex2 C λd2:C.eq C (CHead c1 k u) (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 k u) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C (CHead c1 k u) (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
end of h1
(h2)
consider H4
we proved
eq
C
<λ:C.C> CASE CHead c2 k u OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒c2 | CHead c0 ⇒c0
eq C c2 d1
end of h2
by (h1 h2)
we proved
or3
ex2 C λd2:C.eq C (CHead c1 k u) (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 k u) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C (CHead c1 k u) (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
∀H3:eq C (CHead c2 k u) (CHead d1 (Bind Abbr) u1)
.or3
ex2 C λd2:C.eq C (CHead c1 k u) (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 k u) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C (CHead c1 k u) (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case csuba_void : c1:C c2:C H1:csuba g c1 c2 b:B H3:not (eq B b Void) u0:T u2:T ⇒
the thesis becomes
∀H4:eq C (CHead c2 (Bind b) u2) (CHead d1 (Bind Abbr) u1)
.or3
ex2
C
λd2:C.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu3:T.λ:A.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Abst) u3)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu3:T.λa:A.arity g d2 u3 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2
C
T
λd2:C.λu3:T.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Void) u3)
λd2:C.λ:T.csuba g d2 d1
(H2) by induction hypothesis we know
eq C c2 (CHead d1 (Bind Abbr) u1)
→(or3
ex2 C λd2:C.eq C c1 (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C c1 (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C c1 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
suppose H4: eq C (CHead c2 (Bind b) u2) (CHead d1 (Bind Abbr) u1)
(H5)
by (f_equal . . . . . H4)
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒c2 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead c2 (Bind b) u2)
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead d1 (Bind Abbr) u1)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
B
<λ:C.B>
CASE CHead c2 (Bind b) u2 OF
CSort ⇒b
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
<λ:C.B>
CASE CHead d1 (Bind Abbr) u1 OF
CSort ⇒b
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
eq
B
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
CHead c2 (Bind b) u2
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
CHead d1 (Bind Abbr) u1
end of H6
(H8)
consider H6
we proved
eq
B
<λ:C.B>
CASE CHead c2 (Bind b) u2 OF
CSort ⇒b
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
<λ:C.B>
CASE CHead d1 (Bind Abbr) u1 OF
CSort ⇒b
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
eq B b Abbr
end of H8
suppose H9: eq C c2 d1
(H12)
we proceed by induction on H9 to prove csuba g c1 d1
case refl_equal : ⇒
the thesis becomes the hypothesis H1
csuba g c1 d1
end of H12
by (refl_equal . .)
we proved eq C (CHead c1 (Bind Void) u0) (CHead c1 (Bind Void) u0)
by (ex2_2_intro . . . . . . previous H12)
we proved
ex2_2
C
T
λd2:C.λu3:T.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Void) u3)
λd2:C.λ:T.csuba g d2 d1
by (or3_intro2 . . . previous)
we proved
or3
ex2
C
λd2:C.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu3:T.λ:A.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Abst) u3)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu3:T.λa:A.arity g d2 u3 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2
C
T
λd2:C.λu3:T.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Void) u3)
λd2:C.λ:T.csuba g d2 d1
eq C c2 d1
→(or3
ex2
C
λd2:C.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu3:T.λ:A.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Abst) u3)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu3:T.λa:A.arity g d2 u3 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2
C
T
λd2:C.λu3:T.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Void) u3)
λd2:C.λ:T.csuba g d2 d1)
end of h1
(h2)
consider H5
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒c2 | CHead c0 ⇒c0
eq C c2 d1
end of h2
by (h1 h2)
we proved
or3
ex2
C
λd2:C.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu3:T.λ:A.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Abst) u3)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu3:T.λa:A.arity g d2 u3 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2
C
T
λd2:C.λu3:T.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Void) u3)
λd2:C.λ:T.csuba g d2 d1
∀H4:eq C (CHead c2 (Bind b) u2) (CHead d1 (Bind Abbr) u1)
.or3
ex2
C
λd2:C.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu3:T.λ:A.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Abst) u3)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu3:T.λa:A.arity g d2 u3 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2
C
T
λd2:C.λu3:T.eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Void) u3)
λd2:C.λ:T.csuba g d2 d1
case csuba_abst : c1:C c2:C H1:csuba g c1 c2 t:T a:A H3:arity g c1 t (asucc g a) u:T H4:arity g c2 u a ⇒
the thesis becomes
∀H5:eq C (CHead c2 (Bind Abbr) u) (CHead d1 (Bind Abbr) u1)
.or3
ex2
C
λd2:C.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa0:A.arity g d2 u2 (asucc g a0)
λ:C.λ:T.λa0:A.arity g d1 u1 a0
ex2_2
C
T
λd2:C.λu2:T.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
(H2) by induction hypothesis we know
eq C c2 (CHead d1 (Bind Abbr) u1)
→(or3
ex2 C λd2:C.eq C c1 (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C c1 (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C c1 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
suppose H5: eq C (CHead c2 (Bind Abbr) u) (CHead d1 (Bind Abbr) u1)
(H6)
by (f_equal . . . . . H5)
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind Abbr) u OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒c2 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead c2 (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead d1 (Bind Abbr) u1)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:C.T> CASE CHead c2 (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒u | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead c2 (Bind Abbr) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead d1 (Bind Abbr) u1)
end of H7
suppose H8: eq C c2 d1
(H9)
consider H7
we proved
eq
T
<λ:C.T> CASE CHead c2 (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u u1
we proceed by induction on the previous result to prove arity g c2 u1 a
case refl_equal : ⇒
the thesis becomes the hypothesis H4
arity g c2 u1 a
end of H9
(H10)
we proceed by induction on H8 to prove arity g d1 u1 a
case refl_equal : ⇒
the thesis becomes the hypothesis H9
arity g d1 u1 a
end of H10
(H12)
we proceed by induction on H8 to prove csuba g c1 d1
case refl_equal : ⇒
the thesis becomes the hypothesis H1
csuba g c1 d1
end of H12
by (refl_equal . .)
we proved eq C (CHead c1 (Bind Abst) t) (CHead c1 (Bind Abst) t)
by (ex4_3_intro . . . . . . . . . . previous H12 H3 H10)
we proved
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa0:A.arity g d2 u2 (asucc g a0)
λ:C.λ:T.λa0:A.arity g d1 u1 a0
by (or3_intro1 . . . previous)
we proved
or3
ex2
C
λd2:C.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa0:A.arity g d2 u2 (asucc g a0)
λ:C.λ:T.λa0:A.arity g d1 u1 a0
ex2_2
C
T
λd2:C.λu2:T.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
eq C c2 d1
→(or3
ex2
C
λd2:C.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa0:A.arity g d2 u2 (asucc g a0)
λ:C.λ:T.λa0:A.arity g d1 u1 a0
ex2_2
C
T
λd2:C.λu2:T.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1)
end of h1
(h2)
consider H6
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind Abbr) u OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead d1 (Bind Abbr) u1 OF CSort ⇒c2 | CHead c0 ⇒c0
eq C c2 d1
end of h2
by (h1 h2)
we proved
or3
ex2
C
λd2:C.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa0:A.arity g d2 u2 (asucc g a0)
λ:C.λ:T.λa0:A.arity g d1 u1 a0
ex2_2
C
T
λd2:C.λu2:T.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
∀H5:eq C (CHead c2 (Bind Abbr) u) (CHead d1 (Bind Abbr) u1)
.or3
ex2
C
λd2:C.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abbr) u1)
λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa0:A.arity g d2 u2 (asucc g a0)
λ:C.λ:T.λa0:A.arity g d1 u1 a0
ex2_2
C
T
λd2:C.λu2:T.eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proved
eq C y (CHead d1 (Bind Abbr) u1)
→(or3
ex2 C λd2:C.eq C c (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C c (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C c (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
we proved
∀y:C
.csuba g c y
→(eq C y (CHead d1 (Bind Abbr) u1)
→(or3
ex2 C λd2:C.eq C c (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C c (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C c (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1))
by (insert_eq . . . . previous H)
we proved
or3
ex2 C λd2:C.eq C c (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C c (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C c (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
∀g:G
.∀d1:C
.∀c:C
.∀u1:T
.csuba g c (CHead d1 (Bind Abbr) u1)
→(or3
ex2 C λd2:C.eq C c (CHead d2 (Bind Abbr) u1) λd2:C.csuba g d2 d1
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C c (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d1
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d1 u1 a
ex2_2 C T λd2:C.λu2:T.eq C c (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)