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