DEFINITION arity_gen_abst()
TYPE =
∀g:G
.∀c:C
.∀u:T
.∀t:T
.∀a:A
.arity g c (THead (Bind Abst) u t) a
→(ex3_2
A
A
λa1:A.λa2:A.eq A a (AHead a1 a2)
λa1:A.λ:A.arity g c u (asucc g a1)
λ:A.λa2:A.arity g (CHead c (Bind Abst) u) t a2)
BODY =
assume g: G
assume c: C
assume u: T
assume t: T
assume a: A
suppose H: arity g c (THead (Bind Abst) u t) a
assume y: T
suppose H0: arity g c y a
we proceed by induction on H0 to prove
eq T y (THead (Bind Abst) u t)
→(ex3_2
A
A
λa1:A.λa2:A.eq A a (AHead a1 a2)
λa1:A.λ:A.arity g c u (asucc g a1)
λ:A.λa2:A.arity g (CHead c (Bind Abst) u) t a2)
case arity_sort : c0:C n:nat ⇒
the thesis becomes
∀H1:eq T (TSort n) (THead (Bind Abst) u t)
.ex3_2
A
A
λa1:A.λa2:A.eq A (ASort O n) (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
suppose H1: eq T (TSort n) (THead (Bind Abst) u t)
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H2
consider H2
we proved
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
A
A
λa1:A.λa2:A.eq A (ASort O n) (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
we proved
ex3_2
A
A
λa1:A.λa2:A.eq A (ASort O n) (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
∀H1:eq T (TSort n) (THead (Bind Abst) u t)
.ex3_2
A
A
λa1:A.λa2:A.eq A (ASort O n) (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
case arity_abbr : c0:C d:C u0:T i:nat :getl i c0 (CHead d (Bind Abbr) u0) a0:A :arity g d u0 a0 ⇒
the thesis becomes
∀H4:eq T (TLRef i) (THead (Bind Abst) u t)
.ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
() by induction hypothesis we know
eq T u0 (THead (Bind Abst) u t)
→(ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g d u (asucc g a1)
λ:A.λa2:A.arity g (CHead d (Bind Abst) u) t a2)
suppose H4: eq T (TLRef i) (THead (Bind Abst) u t)
(H5)
we proceed by induction on H4 to prove
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H5
consider H5
we proved
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
we proved
ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
∀H4:eq T (TLRef i) (THead (Bind Abst) u t)
.ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
case arity_abst : c0:C d:C u0:T i:nat :getl i c0 (CHead d (Bind Abst) u0) a0:A :arity g d u0 (asucc g a0) ⇒
the thesis becomes
∀H4:eq T (TLRef i) (THead (Bind Abst) u t)
.ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
() by induction hypothesis we know
eq T u0 (THead (Bind Abst) u t)
→(ex3_2
A
A
λa1:A.λa2:A.eq A (asucc g a0) (AHead a1 a2)
λa1:A.λ:A.arity g d u (asucc g a1)
λ:A.λa2:A.arity g (CHead d (Bind Abst) u) t a2)
suppose H4: eq T (TLRef i) (THead (Bind Abst) u t)
(H5)
we proceed by induction on H4 to prove
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H5
consider H5
we proved
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
we proved
ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
∀H4:eq T (TLRef i) (THead (Bind Abst) u t)
.ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
case arity_bind : b:B H1:not (eq B b Abst) c0:C u0:T a1:A H2:arity g c0 u0 a1 t0:T a2:A H4:arity g (CHead c0 (Bind b) u0) t0 a2 ⇒
the thesis becomes
∀H6:eq T (THead (Bind b) u0 t0) (THead (Bind Abst) u t)
.ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
(H3) by induction hypothesis we know
eq T u0 (THead (Bind Abst) u t)
→(ex3_2
A
A
λa2:A.λa3:A.eq A a1 (AHead a2 a3)
λa2:A.λ:A.arity g c0 u (asucc g a2)
λ:A.λa3:A.arity g (CHead c0 (Bind Abst) u) t a3)
(H5) by induction hypothesis we know
eq T t0 (THead (Bind Abst) u t)
→(ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g (CHead c0 (Bind b) u0) u (asucc g a3)
λ:A.λa4:A.arity g (CHead (CHead c0 (Bind b) u0) (Bind Abst) u) t a4)
suppose H6: eq T (THead (Bind b) u0 t0) (THead (Bind Abst) u t)
(H7)
by (f_equal . . . . . H6)
we proved
eq
B
<λ:T.B>
CASE THead (Bind b) u0 t0 OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
<λ:T.B>
CASE THead (Bind Abst) u t OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
eq
B
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
THead (Bind b) u0 t0
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
THead (Bind Abst) u t
end of H7
(h1)
(H8)
by (f_equal . . . . . H6)
we proved
eq
T
<λ:T.T> CASE THead (Bind b) u0 t0 OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1 (THead (Bind b) u0 t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
THead (Bind Abst) u t
end of H8
(h1)
(H9)
by (f_equal . . . . . H6)
we proved
eq
T
<λ:T.T> CASE THead (Bind b) u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1 (THead (Bind b) u0 t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
THead (Bind Abst) u t
end of H9
suppose H10: eq T u0 u
suppose H11: eq B b Abst
(H12)
consider H9
we proved
eq
T
<λ:T.T> CASE THead (Bind b) u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
that is equivalent to eq T t0 t
we proceed by induction on the previous result to prove
eq T t (THead (Bind Abst) u t)
→(ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g (CHead c0 (Bind b) u0) u (asucc g a3)
λ:A.λa4:A.arity g (CHead (CHead c0 (Bind b) u0) (Bind Abst) u) t a4)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
eq T t (THead (Bind Abst) u t)
→(ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g (CHead c0 (Bind b) u0) u (asucc g a3)
λ:A.λa4:A.arity g (CHead (CHead c0 (Bind b) u0) (Bind Abst) u) t a4)
end of H12
(H13)
consider H9
we proved
eq
T
<λ:T.T> CASE THead (Bind b) u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
that is equivalent to eq T t0 t
we proceed by induction on the previous result to prove arity g (CHead c0 (Bind b) u0) t a2
case refl_equal : ⇒
the thesis becomes the hypothesis H4
arity g (CHead c0 (Bind b) u0) t a2
end of H13
(H14)
we proceed by induction on H10 to prove
eq T t (THead (Bind Abst) u t)
→(ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g (CHead c0 (Bind b) u) u (asucc g a3)
λ:A.λa4:A.arity g (CHead (CHead c0 (Bind b) u) (Bind Abst) u) t a4)
case refl_equal : ⇒
the thesis becomes the hypothesis H12
eq T t (THead (Bind Abst) u t)
→(ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g (CHead c0 (Bind b) u) u (asucc g a3)
λ:A.λa4:A.arity g (CHead (CHead c0 (Bind b) u) (Bind Abst) u) t a4)
end of H14
(H15)
we proceed by induction on H10 to prove arity g (CHead c0 (Bind b) u) t a2
case refl_equal : ⇒
the thesis becomes the hypothesis H13
arity g (CHead c0 (Bind b) u) t a2
end of H15
(H20)
we proceed by induction on H11 to prove not (eq B Abst Abst)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
not (eq B Abst Abst)
end of H20
(H21)
by (refl_equal . .)
we proved eq B Abst Abst
by (H20 previous)
we proved False
by cases on the previous result we prove
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
end of H21
consider H21
we proved
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
eq T u0 u
→(eq B b Abst
→(ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4))
end of h1
(h2)
consider H8
we proved
eq
T
<λ:T.T> CASE THead (Bind b) u0 t0 OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
eq T u0 u
end of h2
by (h1 h2)
eq B b Abst
→(ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4)
end of h1
(h2)
consider H7
we proved
eq
B
<λ:T.B>
CASE THead (Bind b) u0 t0 OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
<λ:T.B>
CASE THead (Bind Abst) u t OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
eq B b Abst
end of h2
by (h1 h2)
we proved
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
∀H6:eq T (THead (Bind b) u0 t0) (THead (Bind Abst) u t)
.ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
case arity_head : c0:C u0:T a1:A H1:arity g c0 u0 (asucc g a1) t0:T a2:A H3:arity g (CHead c0 (Bind Abst) u0) t0 a2 ⇒
the thesis becomes
∀H5:eq T (THead (Bind Abst) u0 t0) (THead (Bind Abst) u t)
.ex3_2
A
A
λa3:A.λa4:A.eq A (AHead a1 a2) (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
(H2) by induction hypothesis we know
eq T u0 (THead (Bind Abst) u t)
→(ex3_2
A
A
λa2:A.λa3:A.eq A (asucc g a1) (AHead a2 a3)
λa2:A.λ:A.arity g c0 u (asucc g a2)
λ:A.λa3:A.arity g (CHead c0 (Bind Abst) u) t a3)
(H4) by induction hypothesis we know
eq T t0 (THead (Bind Abst) u t)
→(ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g (CHead c0 (Bind Abst) u0) u (asucc g a3)
λ:A.λa4:A.arity g (CHead (CHead c0 (Bind Abst) u0) (Bind Abst) u) t a4)
suppose H5: eq T (THead (Bind Abst) u0 t0) (THead (Bind Abst) u t)
(H6)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) u0 t0 OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
THead (Bind Abst) u0 t0
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
THead (Bind Abst) u t
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
THead (Bind Abst) u0 t0
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
THead (Bind Abst) u t
end of H7
suppose H8: eq T u0 u
(H9)
consider H7
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
that is equivalent to eq T t0 t
we proceed by induction on the previous result to prove
eq T t (THead (Bind Abst) u t)
→(ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g (CHead c0 (Bind Abst) u0) u (asucc g a3)
λ:A.λa4:A.arity g (CHead (CHead c0 (Bind Abst) u0) (Bind Abst) u) t a4)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq T t (THead (Bind Abst) u t)
→(ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g (CHead c0 (Bind Abst) u0) u (asucc g a3)
λ:A.λa4:A.arity g (CHead (CHead c0 (Bind Abst) u0) (Bind Abst) u) t a4)
end of H9
(H10)
consider H7
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
that is equivalent to eq T t0 t
we proceed by induction on the previous result to prove arity g (CHead c0 (Bind Abst) u0) t a2
case refl_equal : ⇒
the thesis becomes the hypothesis H3
arity g (CHead c0 (Bind Abst) u0) t a2
end of H10
(H12)
we proceed by induction on H8 to prove arity g (CHead c0 (Bind Abst) u) t a2
case refl_equal : ⇒
the thesis becomes the hypothesis H10
arity g (CHead c0 (Bind Abst) u) t a2
end of H12
(H14)
we proceed by induction on H8 to prove arity g c0 u (asucc g a1)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
arity g c0 u (asucc g a1)
end of H14
by (refl_equal . .)
we proved eq A (AHead a1 a2) (AHead a1 a2)
by (ex3_2_intro . . . . . . . previous H14 H12)
we proved
ex3_2
A
A
λa3:A.λa4:A.eq A (AHead a1 a2) (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
eq T u0 u
→(ex3_2
A
A
λa3:A.λa4:A.eq A (AHead a1 a2) (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4)
end of h1
(h2)
consider H6
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) u0 t0 OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
eq T u0 u
end of h2
by (h1 h2)
we proved
ex3_2
A
A
λa3:A.λa4:A.eq A (AHead a1 a2) (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
∀H5:eq T (THead (Bind Abst) u0 t0) (THead (Bind Abst) u t)
.ex3_2
A
A
λa3:A.λa4:A.eq A (AHead a1 a2) (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
case arity_appl : c0:C u0:T a1:A :arity g c0 u0 a1 t0:T a2:A :arity g c0 t0 (AHead a1 a2) ⇒
the thesis becomes
∀H5:eq T (THead (Flat Appl) u0 t0) (THead (Bind Abst) u t)
.ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
() by induction hypothesis we know
eq T u0 (THead (Bind Abst) u t)
→(ex3_2
A
A
λa2:A.λa3:A.eq A a1 (AHead a2 a3)
λa2:A.λ:A.arity g c0 u (asucc g a2)
λ:A.λa3:A.arity g (CHead c0 (Bind Abst) u) t a3)
() by induction hypothesis we know
eq T t0 (THead (Bind Abst) u t)
→(ex3_2
A
A
λa3:A.λa4:A.eq A (AHead a1 a2) (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4)
suppose H5: eq T (THead (Flat Appl) u0 t0) (THead (Bind Abst) u t)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
end of H6
consider H6
we proved
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead 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
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
we proved
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
∀H5:eq T (THead (Flat Appl) u0 t0) (THead (Bind Abst) u t)
.ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
case arity_cast : c0:C u0:T a0:A :arity g c0 u0 (asucc g a0) t0:T :arity g c0 t0 a0 ⇒
the thesis becomes
∀H5:eq T (THead (Flat Cast) u0 t0) (THead (Bind Abst) u t)
.ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
() by induction hypothesis we know
eq T u0 (THead (Bind Abst) u t)
→(ex3_2
A
A
λa1:A.λa2:A.eq A (asucc g a0) (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2)
() by induction hypothesis we know
eq T t0 (THead (Bind Abst) u t)
→(ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2)
suppose H5: eq T (THead (Flat Cast) u0 t0) (THead (Bind Abst) u t)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Cast) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Cast) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
end of H6
consider H6
we proved
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead 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
ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
we proved
ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
∀H5:eq T (THead (Flat Cast) u0 t0) (THead (Bind Abst) u t)
.ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
case arity_repl : c0:C t0:T a1:A H1:arity g c0 t0 a1 a2:A H3:leq g a1 a2 ⇒
the thesis becomes
∀H4:eq T t0 (THead (Bind Abst) u t)
.ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
(H2) by induction hypothesis we know
eq T t0 (THead (Bind Abst) u t)
→(ex3_2
A
A
λa2:A.λa3:A.eq A a1 (AHead a2 a3)
λa2:A.λ:A.arity g c0 u (asucc g a2)
λ:A.λa3:A.arity g (CHead c0 (Bind Abst) u) t a3)
suppose H4: eq T t0 (THead (Bind Abst) u t)
(H5)
by (f_equal . . . . . H4)
we proved eq T t0 (THead (Bind Abst) u t)
eq T (λe:T.e t0) (λe:T.e (THead (Bind Abst) u t))
end of H5
(H6)
we proceed by induction on H5 to prove
eq T (THead (Bind Abst) u t) (THead (Bind Abst) u t)
→(ex3_2
A
A
λa3:A.λa4:A.eq A a1 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
eq T (THead (Bind Abst) u t) (THead (Bind Abst) u t)
→(ex3_2
A
A
λa3:A.λa4:A.eq A a1 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4)
end of H6
(H7)
we proceed by induction on H5 to prove arity g c0 (THead (Bind Abst) u t) a1
case refl_equal : ⇒
the thesis becomes the hypothesis H1
arity g c0 (THead (Bind Abst) u t) a1
end of H7
(H8)
by (refl_equal . .)
we proved eq T (THead (Bind Abst) u t) (THead (Bind Abst) u t)
by (H6 previous)
ex3_2
A
A
λa3:A.λa4:A.eq A a1 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
end of H8
we proceed by induction on H8 to prove
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
case ex3_2_intro : x0:A x1:A H9:eq A a1 (AHead x0 x1) H10:arity g c0 u (asucc g x0) H11:arity g (CHead c0 (Bind Abst) u) t x1 ⇒
the thesis becomes
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
(H12)
we proceed by induction on H9 to prove leq g (AHead x0 x1) a2
case refl_equal : ⇒
the thesis becomes the hypothesis H3
leq g (AHead x0 x1) a2
end of H12
(H_x)
by (leq_gen_head1 . . . . H12)
ex3_2 A A λa3:A.λ:A.leq g x0 a3 λ:A.λa4:A.leq g x1 a4 λa3:A.λa4:A.eq A a2 (AHead a3 a4)
end of H_x
(H14) consider H_x
we proceed by induction on H14 to prove
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
case ex3_2_intro : x2:A x3:A H15:leq g x0 x2 H16:leq g x1 x3 H17:eq A a2 (AHead x2 x3) ⇒
the thesis becomes
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
(H18)
by (f_equal . . . . . H17)
we proved eq A a2 (AHead x2 x3)
eq A (λe:A.e a2) (λe:A.e (AHead x2 x3))
end of H18
(h1)
by (refl_equal . .)
eq A (AHead x2 x3) (AHead x2 x3)
end of h1
(h2)
by (asucc_repl . . . H15)
we proved leq g (asucc g x0) (asucc g x2)
by (arity_repl . . . . H10 . previous)
arity g c0 u (asucc g x2)
end of h2
(h3)
by (arity_repl . . . . H11 . H16)
arity g (CHead c0 (Bind Abst) u) t x3
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
A
A
λa3:A.λa4:A.eq A (AHead x2 x3) (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
by (eq_ind_r . . . previous . H18)
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
we proved
ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
∀H4:eq T t0 (THead (Bind Abst) u t)
.ex3_2
A
A
λa3:A.λa4:A.eq A a2 (AHead a3 a4)
λa3:A.λ:A.arity g c0 u (asucc g a3)
λ:A.λa4:A.arity g (CHead c0 (Bind Abst) u) t a4
we proved
eq T y (THead (Bind Abst) u t)
→(ex3_2
A
A
λa1:A.λa2:A.eq A a (AHead a1 a2)
λa1:A.λ:A.arity g c u (asucc g a1)
λ:A.λa2:A.arity g (CHead c (Bind Abst) u) t a2)
we proved
∀y:T
.arity g c y a
→(eq T y (THead (Bind Abst) u t)
→(ex3_2
A
A
λa1:A.λa2:A.eq A a (AHead a1 a2)
λa1:A.λ:A.arity g c u (asucc g a1)
λ:A.λa2:A.arity g (CHead c (Bind Abst) u) t a2))
by (insert_eq . . . . previous H)
we proved
ex3_2
A
A
λa1:A.λa2:A.eq A a (AHead a1 a2)
λa1:A.λ:A.arity g c u (asucc g a1)
λ:A.λa2:A.arity g (CHead c (Bind Abst) u) t a2
we proved
∀g:G
.∀c:C
.∀u:T
.∀t:T
.∀a:A
.arity g c (THead (Bind Abst) u t) a
→(ex3_2
A
A
λa1:A.λa2:A.eq A a (AHead a1 a2)
λa1:A.λ:A.arity g c u (asucc g a1)
λ:A.λa2:A.arity g (CHead c (Bind Abst) u) t a2)