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