DEFINITION arity_sred_wcpr0_pr0()
TYPE =
∀g:G.∀c1:C.∀t1:T.∀a:A.(arity g c1 t1 a)→∀c2:C.(wcpr0 c1 c2)→∀t2:T.(pr0 t1 t2)→(arity g c2 t2 a)
BODY =
assume g: G
assume c1: C
assume t1: T
assume a: A
suppose H: arity g c1 t1 a
we proceed by induction on H to prove ∀c2:C.(wcpr0 c1 c2)→∀t2:T.(pr0 t1 t2)→(arity g c2 t2 a)
case arity_sort : c:C n:nat ⇒
the thesis becomes ∀c2:C.(wcpr0 c c2)→∀t2:T.∀H1:(pr0 (TSort n) t2).(arity g c2 t2 (ASort O n))
assume c2: C
suppose : wcpr0 c c2
assume t2: T
suppose H1: pr0 (TSort n) t2
(h1)
by (arity_sort . . .)
arity g c2 (TSort n) (ASort O n)
end of h1
(h2)
by (pr0_gen_sort . . H1)
eq T t2 (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c2 t2 (ASort O n)
∀c2:C.(wcpr0 c c2)→∀t2:T.∀H1:(pr0 (TSort n) t2).(arity g c2 t2 (ASort O n))
case arity_abbr : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abbr) u) a0:A :arity g d u a0 ⇒
the thesis becomes ∀c2:C.∀H3:(wcpr0 c c2).∀t2:T.∀H4:(pr0 (TLRef i) t2).(arity g c2 t2 a0)
(H2) by induction hypothesis we know ∀c2:C.(wcpr0 d c2)→∀t2:T.(pr0 u t2)→(arity g c2 t2 a0)
assume c2: C
suppose H3: wcpr0 c c2
assume t2: T
suppose H4: pr0 (TLRef i) t2
(h1)
by (wcpr0_getl . . H3 . . . . H0)
we proved ex3_2 C T λe2:C.λu2:T.getl i c2 (CHead e2 (Bind Abbr) u2) λe2:C.λ:T.wcpr0 d e2 λ:C.λu2:T.pr0 u u2
we proceed by induction on the previous result to prove arity g c2 (TLRef i) a0
case ex3_2_intro : x0:C x1:T H5:getl i c2 (CHead x0 (Bind Abbr) x1) H6:wcpr0 d x0 H7:pr0 u x1 ⇒
the thesis becomes arity g c2 (TLRef i) a0
by (H2 . H6 . H7)
we proved arity g x0 x1 a0
by (arity_abbr . . . . . H5 . previous)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
end of h1
(h2)
by (pr0_gen_lref . . H4)
eq T t2 (TLRef i)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c2 t2 a0
∀c2:C.∀H3:(wcpr0 c c2).∀t2:T.∀H4:(pr0 (TLRef i) t2).(arity g c2 t2 a0)
case arity_abst : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abst) u) a0:A :arity g d u (asucc g a0) ⇒
the thesis becomes ∀c2:C.∀H3:(wcpr0 c c2).∀t2:T.∀H4:(pr0 (TLRef i) t2).(arity g c2 t2 a0)
(H2) by induction hypothesis we know ∀c2:C.(wcpr0 d c2)→∀t2:T.(pr0 u t2)→(arity g c2 t2 (asucc g a0))
assume c2: C
suppose H3: wcpr0 c c2
assume t2: T
suppose H4: pr0 (TLRef i) t2
(h1)
by (wcpr0_getl . . H3 . . . . H0)
we proved ex3_2 C T λe2:C.λu2:T.getl i c2 (CHead e2 (Bind Abst) u2) λe2:C.λ:T.wcpr0 d e2 λ:C.λu2:T.pr0 u u2
we proceed by induction on the previous result to prove arity g c2 (TLRef i) a0
case ex3_2_intro : x0:C x1:T H5:getl i c2 (CHead x0 (Bind Abst) x1) H6:wcpr0 d x0 H7:pr0 u x1 ⇒
the thesis becomes arity g c2 (TLRef i) a0
by (H2 . H6 . H7)
we proved arity g x0 x1 (asucc g a0)
by (arity_abst . . . . . H5 . previous)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
end of h1
(h2)
by (pr0_gen_lref . . H4)
eq T t2 (TLRef i)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c2 t2 a0
∀c2:C.∀H3:(wcpr0 c c2).∀t2:T.∀H4:(pr0 (TLRef i) t2).(arity g c2 t2 a0)
case arity_bind : b:B H0:not (eq B b Abst) c:C u:T a1:A :arity g c u a1 t:T a2:A H3:arity g (CHead c (Bind b) u) t a2 ⇒
the thesis becomes ∀c2:C.∀H5:(wcpr0 c c2).∀t2:T.∀H6:(pr0 (THead (Bind b) u t) t2).(arity g c2 t2 a2)
(H2) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t2:T.(pr0 u t2)→(arity g c2 t2 a1)
(H4) by induction hypothesis we know ∀c2:C.(wcpr0 (CHead c (Bind b) u) c2)→∀t2:T.(pr0 t t2)→(arity g c2 t2 a2)
assume c2: C
suppose H5: wcpr0 c c2
assume t2: T
suppose H6: pr0 (THead (Bind b) u t) t2
assume y: T
suppose H7: pr0 y t2
we proceed by induction on H7 to prove (eq T y (THead (Bind b) u t))→(arity g c2 t2 a2)
case pr0_refl : t0:T ⇒
the thesis becomes ∀H8:(eq T t0 (THead (Bind b) u t)).(arity g c2 t0 a2)
suppose H8: eq T t0 (THead (Bind b) u t)
(H9)
by (f_equal . . . . . H8)
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 H9
(h1)
by (pr0_refl .)
we proved pr0 u u
by (H2 . H5 . previous)
arity g c2 u a1
end of h1
(h2)
(h1)
by (pr0_refl .)
we proved pr0 u u
by (wcpr0_comp . . H5 . . previous .)
wcpr0 (CHead c (Bind b) u) (CHead c2 (Bind b) u)
end of h1
(h2) by (pr0_refl .) we proved pr0 t t
by (H4 . h1 . h2)
arity g (CHead c2 (Bind b) u) t a2
end of h2
by (arity_bind . . H0 . . . h1 . . h2)
we proved arity g c2 (THead (Bind b) u t) a2
by (eq_ind_r . . . previous . H9)
we proved arity g c2 t0 a2
∀H8:(eq T t0 (THead (Bind b) u t)).(arity g c2 t0 a2)
case pr0_comp : u1:T u2:T H8:pr0 u1 u2 t3:T t4:T H10:pr0 t3 t4 k:K ⇒
the thesis becomes ∀H12:(eq T (THead k u1 t3) (THead (Bind b) u t)).(arity g c2 (THead k u2 t4) a2)
(H9) by induction hypothesis we know (eq T u1 (THead (Bind b) u t))→(arity g c2 u2 a2)
(H11) by induction hypothesis we know (eq T t3 (THead (Bind b) u t))→(arity g c2 t4 a2)
suppose H12: eq T (THead k u1 t3) (THead (Bind b) u t)
(H13)
by (f_equal . . . . . H12)
we proved
eq
K
<λ:T.K> CASE THead k u1 t3 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K> CASE THead (Bind b) u t OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0 (THead k u1 t3)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
THead (Bind b) u t
end of H13
(h1)
(H14)
by (f_equal . . . . . H12)
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind b) u t OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0 (THead k u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
THead (Bind b) u t
end of H14
(h1)
(H15)
by (f_equal . . . . . H12)
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Bind b) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0 (THead k u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
THead (Bind b) u t
end of H15
suppose H16: eq T u1 u
suppose H17: eq K k (Bind b)
(H19)
consider H15
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Bind b) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
that is equivalent to eq T t3 t
we proceed by induction on the previous result to prove pr0 t t4
case refl_equal : ⇒
the thesis becomes the hypothesis H10
pr0 t t4
end of H19
(H21)
we proceed by induction on H16 to prove pr0 u u2
case refl_equal : ⇒
the thesis becomes the hypothesis H8
pr0 u u2
end of H21
(h1) by (H2 . H5 . H21) we proved arity g c2 u2 a1
(h2)
by (wcpr0_comp . . H5 . . H21 .)
we proved wcpr0 (CHead c (Bind b) u) (CHead c2 (Bind b) u2)
by (H4 . previous . H19)
arity g (CHead c2 (Bind b) u2) t4 a2
end of h2
by (arity_bind . . H0 . . . h1 . . h2)
we proved arity g c2 (THead (Bind b) u2 t4) a2
by (eq_ind_r . . . previous . H17)
we proved arity g c2 (THead k u2 t4) a2
(eq T u1 u)→(eq K k (Bind b))→(arity g c2 (THead k u2 t4) a2)
end of h1
(h2)
consider H14
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind b) u t OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
eq T u1 u
end of h2
by (h1 h2)
(eq K k (Bind b))→(arity g c2 (THead k u2 t4) a2)
end of h1
(h2)
consider H13
we proved
eq
K
<λ:T.K> CASE THead k u1 t3 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K> CASE THead (Bind b) u t OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
eq K k (Bind b)
end of h2
by (h1 h2)
we proved arity g c2 (THead k u2 t4) a2
∀H12:(eq T (THead k u1 t3) (THead (Bind b) u t)).(arity g c2 (THead k u2 t4) a2)
case pr0_beta : u0:T v1:T v2:T :pr0 v1 v2 t3:T t4:T :pr0 t3 t4 ⇒
the thesis becomes
∀H12:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Bind b) u t
.arity g c2 (THead (Bind Abbr) v2 t4) a2
() by induction hypothesis we know (eq T v1 (THead (Bind b) u t))→(arity g c2 v2 a2)
() by induction hypothesis we know (eq T t3 (THead (Bind b) u t))→(arity g c2 t4 a2)
suppose H12:
eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Bind b) u t
(H13)
we proceed by induction on H12 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) v1 (THead (Bind Abst) u0 t3) 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) v1 (THead (Bind Abst) u0 t3) 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 H13
consider H13
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 arity g c2 (THead (Bind Abbr) v2 t4) a2
we proved arity g c2 (THead (Bind Abbr) v2 t4) a2
∀H12:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Bind b) u t
.arity g c2 (THead (Bind Abbr) v2 t4) a2
case pr0_upsilon : b0:B :not (eq B b0 Abst) v1:T v2:T :pr0 v1 v2 u1:T u2:T :pr0 u1 u2 t3:T t4:T :pr0 t3 t4 ⇒
the thesis becomes
∀H15:eq
T
THead (Flat Appl) v1 (THead (Bind b0) u1 t3)
THead (Bind b) u t
.arity
g
c2
THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2
() by induction hypothesis we know (eq T v1 (THead (Bind b) u t))→(arity g c2 v2 a2)
() by induction hypothesis we know (eq T u1 (THead (Bind b) u t))→(arity g c2 u2 a2)
() by induction hypothesis we know (eq T t3 (THead (Bind b) u t))→(arity g c2 t4 a2)
suppose H15:
eq
T
THead (Flat Appl) v1 (THead (Bind b0) u1 t3)
THead (Bind b) u t
(H16)
we proceed by induction on H15 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) v1 (THead (Bind b0) u1 t3) 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) v1 (THead (Bind b0) u1 t3) 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 H16
consider H16
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
arity
g
c2
THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2
we proved
arity
g
c2
THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2
∀H15:eq
T
THead (Flat Appl) v1 (THead (Bind b0) u1 t3)
THead (Bind b) u t
.arity
g
c2
THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2
case pr0_delta : u1:T u2:T H8:pr0 u1 u2 t3:T t4:T H10:pr0 t3 t4 w:T H12:subst0 O u2 t4 w ⇒
the thesis becomes
∀H13:eq T (THead (Bind Abbr) u1 t3) (THead (Bind b) u t)
.arity g c2 (THead (Bind Abbr) u2 w) a2
(H9) by induction hypothesis we know (eq T u1 (THead (Bind b) u t))→(arity g c2 u2 a2)
(H11) by induction hypothesis we know (eq T t3 (THead (Bind b) u t))→(arity g c2 t4 a2)
suppose H13: eq T (THead (Bind Abbr) u1 t3) (THead (Bind b) u t)
(H14)
by (f_equal . . . . . H13)
we proved
eq
B
<λ:T.B>
CASE THead (Bind Abbr) u1 t3 OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:T.B>
CASE THead (Bind b) u t OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
eq
B
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
THead (Bind Abbr) u1 t3
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
THead (Bind b) u t
end of H14
(h1)
(H15)
by (f_equal . . . . . H13)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind b) u t OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
THead (Bind Abbr) u1 t3
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
THead (Bind b) u t
end of H15
(h1)
(H16)
by (f_equal . . . . . H13)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Bind b) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
THead (Bind Abbr) u1 t3
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
THead (Bind b) u t
end of H16
suppose H17: eq T u1 u
suppose H18: eq B Abbr b
(H19)
consider H16
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Bind b) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
that is equivalent to eq T t3 t
we proceed by induction on the previous result to prove (eq T t (THead (Bind b) u t))→(arity g c2 t4 a2)
case refl_equal : ⇒
the thesis becomes the hypothesis H11
(eq T t (THead (Bind b) u t))→(arity g c2 t4 a2)
end of H19
(H20)
consider H16
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Bind b) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
that is equivalent to eq T t3 t
we proceed by induction on the previous result to prove pr0 t t4
case refl_equal : ⇒
the thesis becomes the hypothesis H10
pr0 t t4
end of H20
(H21)
we proceed by induction on H17 to prove (eq T u (THead (Bind b) u t))→(arity g c2 u2 a2)
case refl_equal : ⇒
the thesis becomes the hypothesis H9
(eq T u (THead (Bind b) u t))→(arity g c2 u2 a2)
end of H21
(H22)
we proceed by induction on H17 to prove pr0 u u2
case refl_equal : ⇒
the thesis becomes the hypothesis H8
pr0 u u2
end of H22
(H25)
by (eq_ind_r . . . H4 . H18)
∀c3:C.(wcpr0 (CHead c (Bind Abbr) u) c3)→∀t5:T.(pr0 t t5)→(arity g c3 t5 a2)
end of H25
(H27)
by (eq_ind_r . . . H0 . H18)
not (eq B Abbr Abst)
end of H27
(h1) by (H2 . H5 . H22) we proved arity g c2 u2 a1
(h2)
(h1)
by (wcpr0_comp . . H5 . . H22 .)
we proved wcpr0 (CHead c (Bind Abbr) u) (CHead c2 (Bind Abbr) u2)
by (H25 . previous . H20)
arity g (CHead c2 (Bind Abbr) u2) t4 a2
end of h1
(h2)
by (getl_refl . . .)
getl O (CHead c2 (Bind Abbr) u2) (CHead c2 (Bind Abbr) u2)
end of h2
by (arity_subst0 . . . . h1 . . . h2 . H12)
arity g (CHead c2 (Bind Abbr) u2) w a2
end of h2
by (arity_bind . . H27 . . . h1 . . h2)
we proved arity g c2 (THead (Bind Abbr) u2 w) a2
eq T u1 u
→(eq B Abbr b)→(arity g c2 (THead (Bind Abbr) u2 w) a2)
end of h1
(h2)
consider H15
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind b) u t OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
eq T u1 u
end of h2
by (h1 h2)
(eq B Abbr b)→(arity g c2 (THead (Bind Abbr) u2 w) a2)
end of h1
(h2)
consider H14
we proved
eq
B
<λ:T.B>
CASE THead (Bind Abbr) u1 t3 OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:T.B>
CASE THead (Bind b) u t OF
TSort ⇒Abbr
| TLRef ⇒Abbr
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
eq B Abbr b
end of h2
by (h1 h2)
we proved arity g c2 (THead (Bind Abbr) u2 w) a2
∀H13:eq T (THead (Bind Abbr) u1 t3) (THead (Bind b) u t)
.arity g c2 (THead (Bind Abbr) u2 w) a2
case pr0_zeta : b0:B H8:not (eq B b0 Abst) t3:T t4:T H9:pr0 t3 t4 u0:T ⇒
the thesis becomes
∀H11:eq T (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) u t)
.arity g c2 t4 a2
(H10) by induction hypothesis we know (eq T t3 (THead (Bind b) u t))→(arity g c2 t4 a2)
suppose H11: eq T (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) u t)
(H12)
by (f_equal . . . . . H11)
we proved
eq
B
<λ:T.B>
CASE THead (Bind b0) u0 (lift (S O) O t3) 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 (lift (S O) O t3)
λ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 H12
(h1)
(H13)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T>
CASE THead (Bind b0) u0 (lift (S O) O t3) OF
TSort ⇒u0
| TLRef ⇒u0
| THead t0 ⇒t0
<λ:T.T> CASE THead (Bind b) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
THead (Bind b0) u0 (lift (S O) O t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
THead (Bind b) u t
end of H13
(h1)
(H14)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T>
CASE THead (Bind b0) u0 (lift (S O) O t3) OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| THead t0⇒t0
<λ:T.T>
CASE THead (Bind b) u t OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| THead t0⇒t0
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| THead t0⇒t0
THead (Bind b0) u0 (lift (S O) O t3)
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| THead t0⇒t0
THead (Bind b) u t
end of H14
suppose : eq T u0 u
suppose H16: eq B b0 b
(H19)
consider H14
we proved
eq
T
<λ:T.T>
CASE THead (Bind b0) u0 (lift (S O) O t3) OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| THead t0⇒t0
<λ:T.T>
CASE THead (Bind b) u t OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| THead t0⇒t0
that is equivalent to eq T (lift (S O) O t3) t
by (eq_ind_r . . . H4 . previous)
∀c3:C
.wcpr0 (CHead c (Bind b) u) c3
→∀t5:T.(pr0 (lift (S O) O t3) t5)→(arity g c3 t5 a2)
end of H19
(h1)
(h1)
by (pr0_refl .)
we proved pr0 u u
by (wcpr0_comp . . H5 . . previous .)
wcpr0 (CHead c (Bind b) u) (CHead c2 (Bind b) u)
end of h1
(h2)
by (pr0_lift . . H9 . .)
pr0 (lift (S O) O t3) (lift (S O) O t4)
end of h2
by (H19 . h1 . h2)
arity g (CHead c2 (Bind b) u) (lift (S O) O t4) a2
end of h1
(h2)
by (drop_refl .)
we proved drop O O c2 c2
that is equivalent to drop (r (Bind b) O) O c2 c2
by (drop_drop . . . . previous .)
drop (S O) O (CHead c2 (Bind b) u) c2
end of h2
by (arity_gen_lift . . . . . . h1 . h2)
we proved arity g c2 t4 a2
(eq T u0 u)→(eq B b0 b)→(arity g c2 t4 a2)
end of h1
(h2)
consider H13
we proved
eq
T
<λ:T.T>
CASE THead (Bind b0) u0 (lift (S O) O t3) OF
TSort ⇒u0
| TLRef ⇒u0
| THead t0 ⇒t0
<λ:T.T> CASE THead (Bind b) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
eq T u0 u
end of h2
by (h1 h2)
(eq B b0 b)→(arity g c2 t4 a2)
end of h1
(h2)
consider H12
we proved
eq
B
<λ:T.B>
CASE THead (Bind b0) u0 (lift (S O) O t3) 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 arity g c2 t4 a2
∀H11:eq T (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) u t)
.arity g c2 t4 a2
case pr0_tau : t3:T t4:T :pr0 t3 t4 u0:T ⇒
the thesis becomes ∀H10:(eq T (THead (Flat Cast) u0 t3) (THead (Bind b) u t)).(arity g c2 t4 a2)
() by induction hypothesis we know (eq T t3 (THead (Bind b) u t))→(arity g c2 t4 a2)
suppose H10: eq T (THead (Flat Cast) u0 t3) (THead (Bind b) u t)
(H11)
we proceed by induction on H10 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 t3 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 t3 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 H11
consider H11
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 arity g c2 t4 a2
we proved arity g c2 t4 a2
∀H10:(eq T (THead (Flat Cast) u0 t3) (THead (Bind b) u t)).(arity g c2 t4 a2)
we proved (eq T y (THead (Bind b) u t))→(arity g c2 t2 a2)
we proved ∀y:T.(pr0 y t2)→(eq T y (THead (Bind b) u t))→(arity g c2 t2 a2)
by (insert_eq . . . . previous H6)
we proved arity g c2 t2 a2
∀c2:C.∀H5:(wcpr0 c c2).∀t2:T.∀H6:(pr0 (THead (Bind b) u t) t2).(arity g c2 t2 a2)
case arity_head : c:C u:T a1:A :arity g c u (asucc g a1) t:T a2:A H2:arity g (CHead c (Bind Abst) u) t a2 ⇒
the thesis becomes ∀c2:C.∀H4:(wcpr0 c c2).∀t2:T.∀H5:(pr0 (THead (Bind Abst) u t) t2).(arity g c2 t2 (AHead a1 a2))
(H1) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t2:T.(pr0 u t2)→(arity g c2 t2 (asucc g a1))
(H3) by induction hypothesis we know ∀c2:C.(wcpr0 (CHead c (Bind Abst) u) c2)→∀t2:T.(pr0 t t2)→(arity g c2 t2 a2)
assume c2: C
suppose H4: wcpr0 c c2
assume t2: T
suppose H5: pr0 (THead (Bind Abst) u t) t2
assume y: T
suppose H6: pr0 y t2
we proceed by induction on H6 to prove (eq T y (THead (Bind Abst) u t))→(arity g c2 t2 (AHead a1 a2))
case pr0_refl : t0:T ⇒
the thesis becomes ∀H7:(eq T t0 (THead (Bind Abst) u t)).(arity g c2 t0 (AHead a1 a2))
suppose H7: eq T t0 (THead (Bind Abst) u t)
(H8)
by (f_equal . . . . . H7)
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 H8
(h1)
by (pr0_refl .)
we proved pr0 u u
by (H1 . H4 . previous)
arity g c2 u (asucc g a1)
end of h1
(h2)
(h1)
by (pr0_refl .)
we proved pr0 u u
by (wcpr0_comp . . H4 . . previous .)
wcpr0 (CHead c (Bind Abst) u) (CHead c2 (Bind Abst) u)
end of h1
(h2) by (pr0_refl .) we proved pr0 t t
by (H3 . h1 . h2)
arity g (CHead c2 (Bind Abst) u) t a2
end of h2
by (arity_head . . . . h1 . . h2)
we proved arity g c2 (THead (Bind Abst) u t) (AHead a1 a2)
by (eq_ind_r . . . previous . H8)
we proved arity g c2 t0 (AHead a1 a2)
∀H7:(eq T t0 (THead (Bind Abst) u t)).(arity g c2 t0 (AHead a1 a2))
case pr0_comp : u1:T u2:T H7:pr0 u1 u2 t3:T t4:T H9:pr0 t3 t4 k:K ⇒
the thesis becomes
∀H11:eq T (THead k u1 t3) (THead (Bind Abst) u t)
.arity g c2 (THead k u2 t4) (AHead a1 a2)
(H8) by induction hypothesis we know (eq T u1 (THead (Bind Abst) u t))→(arity g c2 u2 (AHead a1 a2))
(H10) by induction hypothesis we know (eq T t3 (THead (Bind Abst) u t))→(arity g c2 t4 (AHead a1 a2))
suppose H11: eq T (THead k u1 t3) (THead (Bind Abst) u t)
(H12)
by (f_equal . . . . . H11)
we proved
eq
K
<λ:T.K> CASE THead k u1 t3 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Bind Abst) u t OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0 (THead k u1 t3)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
THead (Bind Abst) u t
end of H12
(h1)
(H13)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0 (THead k u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
THead (Bind Abst) u t
end of H13
(h1)
(H14)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0 (THead k u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
THead (Bind Abst) u t
end of H14
suppose H15: eq T u1 u
suppose H16: eq K k (Bind Abst)
(H18)
consider H14
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
that is equivalent to eq T t3 t
we proceed by induction on the previous result to prove pr0 t t4
case refl_equal : ⇒
the thesis becomes the hypothesis H9
pr0 t t4
end of H18
(H20)
we proceed by induction on H15 to prove pr0 u u2
case refl_equal : ⇒
the thesis becomes the hypothesis H7
pr0 u u2
end of H20
(h1)
by (H1 . H4 . H20)
arity g c2 u2 (asucc g a1)
end of h1
(h2)
by (wcpr0_comp . . H4 . . H20 .)
we proved wcpr0 (CHead c (Bind Abst) u) (CHead c2 (Bind Abst) u2)
by (H3 . previous . H18)
arity g (CHead c2 (Bind Abst) u2) t4 a2
end of h2
by (arity_head . . . . h1 . . h2)
we proved arity g c2 (THead (Bind Abst) u2 t4) (AHead a1 a2)
by (eq_ind_r . . . previous . H16)
we proved arity g c2 (THead k u2 t4) (AHead a1 a2)
eq T u1 u
→(eq K k (Bind Abst))→(arity g c2 (THead k u2 t4) (AHead a1 a2))
end of h1
(h2)
consider H13
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
eq T u1 u
end of h2
by (h1 h2)
(eq K k (Bind Abst))→(arity g c2 (THead k u2 t4) (AHead a1 a2))
end of h1
(h2)
consider H12
we proved
eq
K
<λ:T.K> CASE THead k u1 t3 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Bind Abst) u t OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
eq K k (Bind Abst)
end of h2
by (h1 h2)
we proved arity g c2 (THead k u2 t4) (AHead a1 a2)
∀H11:eq T (THead k u1 t3) (THead (Bind Abst) u t)
.arity g c2 (THead k u2 t4) (AHead a1 a2)
case pr0_beta : u0:T v1:T v2:T :pr0 v1 v2 t3:T t4:T :pr0 t3 t4 ⇒
the thesis becomes
∀H11:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Bind Abst) u t
.arity g c2 (THead (Bind Abbr) v2 t4) (AHead a1 a2)
() by induction hypothesis we know (eq T v1 (THead (Bind Abst) u t))→(arity g c2 v2 (AHead a1 a2))
() by induction hypothesis we know (eq T t3 (THead (Bind Abst) u t))→(arity g c2 t4 (AHead a1 a2))
suppose H11:
eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Bind Abst) u t
(H12)
we proceed by induction on H11 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) v1 (THead (Bind Abst) u0 t3) 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) v1 (THead (Bind Abst) u0 t3) 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 H12
consider H12
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 arity g c2 (THead (Bind Abbr) v2 t4) (AHead a1 a2)
we proved arity g c2 (THead (Bind Abbr) v2 t4) (AHead a1 a2)
∀H11:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Bind Abst) u t
.arity g c2 (THead (Bind Abbr) v2 t4) (AHead a1 a2)
case pr0_upsilon : b:B :not (eq B b Abst) v1:T v2:T :pr0 v1 v2 u1:T u2:T :pr0 u1 u2 t3:T t4:T :pr0 t3 t4 ⇒
the thesis becomes
∀H14:eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Bind Abst) u t
.arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
AHead a1 a2
() by induction hypothesis we know (eq T v1 (THead (Bind Abst) u t))→(arity g c2 v2 (AHead a1 a2))
() by induction hypothesis we know (eq T u1 (THead (Bind Abst) u t))→(arity g c2 u2 (AHead a1 a2))
() by induction hypothesis we know (eq T t3 (THead (Bind Abst) u t))→(arity g c2 t4 (AHead a1 a2))
suppose H14:
eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Bind Abst) u t
(H15)
we proceed by induction on H14 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) v1 (THead (Bind b) u1 t3) 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) v1 (THead (Bind b) u1 t3) 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 H15
consider H15
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
arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
AHead a1 a2
we proved
arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
AHead a1 a2
∀H14:eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Bind Abst) u t
.arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
AHead a1 a2
case pr0_delta : u1:T u2:T :pr0 u1 u2 t3:T t4:T :pr0 t3 t4 w:T :subst0 O u2 t4 w ⇒
the thesis becomes
∀H12:eq T (THead (Bind Abbr) u1 t3) (THead (Bind Abst) u t)
.arity g c2 (THead (Bind Abbr) u2 w) (AHead a1 a2)
() by induction hypothesis we know (eq T u1 (THead (Bind Abst) u t))→(arity g c2 u2 (AHead a1 a2))
() by induction hypothesis we know (eq T t3 (THead (Bind Abst) u t))→(arity g c2 t4 (AHead a1 a2))
suppose H12: eq T (THead (Bind Abbr) u1 t3) (THead (Bind Abst) u t)
(H13)
we proceed by induction on H12 to prove
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind Abbr) u1 t3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind Abbr) u1 t3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
end of H13
consider H13
we proved
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove arity g c2 (THead (Bind Abbr) u2 w) (AHead a1 a2)
we proved arity g c2 (THead (Bind Abbr) u2 w) (AHead a1 a2)
∀H12:eq T (THead (Bind Abbr) u1 t3) (THead (Bind Abst) u t)
.arity g c2 (THead (Bind Abbr) u2 w) (AHead a1 a2)
case pr0_zeta : b:B H7:not (eq B b Abst) t3:T t4:T :pr0 t3 t4 u0:T ⇒
the thesis becomes
∀H10:eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Bind Abst) u t
.arity g c2 t4 (AHead a1 a2)
(H9) by induction hypothesis we know (eq T t3 (THead (Bind Abst) u t))→(arity g c2 t4 (AHead a1 a2))
suppose H10:
eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Bind Abst) u t
(H11)
by (f_equal . . . . . H10)
we proved
eq
B
<λ:T.B>
CASE THead (Bind b) u0 (lift (S O) O t3) 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 (lift (S O) O t3)
λ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 H11
(h1)
(H12)
by (f_equal . . . . . H10)
we proved
eq
T
<λ:T.T>
CASE THead (Bind b) u0 (lift (S O) O t3) OF
TSort ⇒u0
| TLRef ⇒u0
| THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
THead (Bind b) u0 (lift (S O) O t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
THead (Bind Abst) u t
end of H12
(h1)
(H13)
by (f_equal . . . . . H10)
we proved
eq
T
<λ:T.T>
CASE THead (Bind b) u0 (lift (S O) O t3) OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| THead t0⇒t0
<λ:T.T>
CASE THead (Bind Abst) u t OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| THead t0⇒t0
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| THead t0⇒t0
THead (Bind b) u0 (lift (S O) O t3)
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt5:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u1 t5⇒THead k (lref_map f d u1) (lref_map f (s k d) t5)
}
λx:nat.plus x (S O)
O
t3
| THead t0⇒t0
THead (Bind Abst) u t
end of H13
suppose : eq T u0 u
suppose H15: eq B b Abst
(H16)
we proceed by induction on H15 to prove not (eq B Abst Abst)
case refl_equal : ⇒
the thesis becomes the hypothesis H7
not (eq B Abst Abst)
end of H16
(H20)
by (refl_equal . .)
we proved eq B Abst Abst
by (H16 previous)
we proved False
by cases on the previous result we prove arity g c2 t4 (AHead a1 a2)
arity g c2 t4 (AHead a1 a2)
end of H20
consider H20
we proved arity g c2 t4 (AHead a1 a2)
(eq T u0 u)→(eq B b Abst)→(arity g c2 t4 (AHead a1 a2))
end of h1
(h2)
consider H12
we proved
eq
T
<λ:T.T>
CASE THead (Bind b) u0 (lift (S O) O t3) OF
TSort ⇒u0
| TLRef ⇒u0
| THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
eq T u0 u
end of h2
by (h1 h2)
(eq B b Abst)→(arity g c2 t4 (AHead a1 a2))
end of h1
(h2)
consider H11
we proved
eq
B
<λ:T.B>
CASE THead (Bind b) u0 (lift (S O) O t3) 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 arity g c2 t4 (AHead a1 a2)
∀H10:eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Bind Abst) u t
.arity g c2 t4 (AHead a1 a2)
case pr0_tau : t3:T t4:T :pr0 t3 t4 u0:T ⇒
the thesis becomes
∀H9:eq T (THead (Flat Cast) u0 t3) (THead (Bind Abst) u t)
.arity g c2 t4 (AHead a1 a2)
() by induction hypothesis we know (eq T t3 (THead (Bind Abst) u t))→(arity g c2 t4 (AHead a1 a2))
suppose H9: eq T (THead (Flat Cast) u0 t3) (THead (Bind Abst) u t)
(H10)
we proceed by induction on H9 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 t3 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 t3 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 H10
consider H10
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 arity g c2 t4 (AHead a1 a2)
we proved arity g c2 t4 (AHead a1 a2)
∀H9:eq T (THead (Flat Cast) u0 t3) (THead (Bind Abst) u t)
.arity g c2 t4 (AHead a1 a2)
we proved (eq T y (THead (Bind Abst) u t))→(arity g c2 t2 (AHead a1 a2))
we proved
∀y:T
.pr0 y t2
→(eq T y (THead (Bind Abst) u t))→(arity g c2 t2 (AHead a1 a2))
by (insert_eq . . . . previous H5)
we proved arity g c2 t2 (AHead a1 a2)
∀c2:C.∀H4:(wcpr0 c c2).∀t2:T.∀H5:(pr0 (THead (Bind Abst) u t) t2).(arity g c2 t2 (AHead a1 a2))
case arity_appl : c:C u:T a1:A :arity g c u a1 t:T a2:A H2:arity g c t (AHead a1 a2) ⇒
the thesis becomes ∀c2:C.∀H4:(wcpr0 c c2).∀t2:T.∀H5:(pr0 (THead (Flat Appl) u t) t2).(arity g c2 t2 a2)
(H1) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t2:T.(pr0 u t2)→(arity g c2 t2 a1)
(H3) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t2:T.(pr0 t t2)→(arity g c2 t2 (AHead a1 a2))
assume c2: C
suppose H4: wcpr0 c c2
assume t2: T
suppose H5: pr0 (THead (Flat Appl) u t) t2
assume y: T
suppose H6: pr0 y t2
we proceed by induction on H6 to prove (eq T y (THead (Flat Appl) u t))→(arity g c2 t2 a2)
case pr0_refl : t0:T ⇒
the thesis becomes ∀H7:(eq T t0 (THead (Flat Appl) u t)).(arity g c2 t0 a2)
suppose H7: eq T t0 (THead (Flat Appl) u t)
(H8)
by (f_equal . . . . . H7)
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 H8
(h1)
by (pr0_refl .)
we proved pr0 u u
by (H1 . H4 . previous)
arity g c2 u a1
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t t
by (H3 . H4 . previous)
arity g c2 t (AHead a1 a2)
end of h2
by (arity_appl . . . . h1 . . h2)
we proved arity g c2 (THead (Flat Appl) u t) a2
by (eq_ind_r . . . previous . H8)
we proved arity g c2 t0 a2
∀H7:(eq T t0 (THead (Flat Appl) u t)).(arity g c2 t0 a2)
case pr0_comp : u1:T u2:T H7:pr0 u1 u2 t3:T t4:T H9:pr0 t3 t4 k:K ⇒
the thesis becomes ∀H11:(eq T (THead k u1 t3) (THead (Flat Appl) u t)).(arity g c2 (THead k u2 t4) a2)
(H8) by induction hypothesis we know (eq T u1 (THead (Flat Appl) u t))→(arity g c2 u2 a2)
(H10) by induction hypothesis we know (eq T t3 (THead (Flat Appl) u t))→(arity g c2 t4 a2)
suppose H11: eq T (THead k u1 t3) (THead (Flat Appl) u t)
(H12)
by (f_equal . . . . . H11)
we proved
eq
K
<λ:T.K> CASE THead k u1 t3 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Flat Appl) u t OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0 (THead k u1 t3)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
THead (Flat Appl) u t
end of H12
(h1)
(H13)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Appl) u t OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0 (THead k u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
THead (Flat Appl) u t
end of H13
(h1)
(H14)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Flat Appl) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0 (THead k u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
THead (Flat Appl) u t
end of H14
suppose H15: eq T u1 u
suppose H16: eq K k (Flat Appl)
(H18)
consider H14
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Flat Appl) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
that is equivalent to eq T t3 t
we proceed by induction on the previous result to prove pr0 t t4
case refl_equal : ⇒
the thesis becomes the hypothesis H9
pr0 t t4
end of H18
(H20)
we proceed by induction on H15 to prove pr0 u u2
case refl_equal : ⇒
the thesis becomes the hypothesis H7
pr0 u u2
end of H20
(h1) by (H1 . H4 . H20) we proved arity g c2 u2 a1
(h2)
by (H3 . H4 . H18)
arity g c2 t4 (AHead a1 a2)
end of h2
by (arity_appl . . . . h1 . . h2)
we proved arity g c2 (THead (Flat Appl) u2 t4) a2
by (eq_ind_r . . . previous . H16)
we proved arity g c2 (THead k u2 t4) a2
(eq T u1 u)→(eq K k (Flat Appl))→(arity g c2 (THead k u2 t4) a2)
end of h1
(h2)
consider H13
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Appl) u t OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
eq T u1 u
end of h2
by (h1 h2)
(eq K k (Flat Appl))→(arity g c2 (THead k u2 t4) a2)
end of h1
(h2)
consider H12
we proved
eq
K
<λ:T.K> CASE THead k u1 t3 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Flat Appl) u t OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
eq K k (Flat Appl)
end of h2
by (h1 h2)
we proved arity g c2 (THead k u2 t4) a2
∀H11:(eq T (THead k u1 t3) (THead (Flat Appl) u t)).(arity g c2 (THead k u2 t4) a2)
case pr0_beta : u0:T v1:T v2:T H7:pr0 v1 v2 t3:T t4:T H9:pr0 t3 t4 ⇒
the thesis becomes
∀H11:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Flat Appl) u t
.arity g c2 (THead (Bind Abbr) v2 t4) a2
(H8) by induction hypothesis we know (eq T v1 (THead (Flat Appl) u t))→(arity g c2 v2 a2)
(H10) by induction hypothesis we know (eq T t3 (THead (Flat Appl) u t))→(arity g c2 t4 a2)
suppose H11:
eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Flat Appl) u t
(H12)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t3) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Appl) u t OF TSort ⇒v1 | TLRef ⇒v1 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t0 ⇒t0
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t0 ⇒t0
THead (Flat Appl) u t
end of H12
(h1)
(H13)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t3) OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) u t OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t0⇒t0
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t0⇒t0
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t0⇒t0
THead (Flat Appl) u t
end of H13
suppose H14: eq T v1 u
(H15)
we proceed by induction on H14 to prove (eq T u (THead (Flat Appl) u t))→(arity g c2 v2 a2)
case refl_equal : ⇒
the thesis becomes the hypothesis H8
(eq T u (THead (Flat Appl) u t))→(arity g c2 v2 a2)
end of H15
(H16)
we proceed by induction on H14 to prove pr0 u v2
case refl_equal : ⇒
the thesis becomes the hypothesis H7
pr0 u v2
end of H16
(H19)
consider H13
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t3) OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) u t OF
TSort ⇒THead (Bind Abst) u0 t3
| TLRef ⇒THead (Bind Abst) u0 t3
| THead t0⇒t0
that is equivalent to eq T (THead (Bind Abst) u0 t3) t
by (eq_ind_r . . . H3 . previous)
∀c3:C.(wcpr0 c c3)→∀t5:T.(pr0 (THead (Bind Abst) u0 t3) t5)→(arity g c3 t5 (AHead a1 a2))
end of H19
(H21) by (H1 . H4 . H16) we proved arity g c2 v2 a1
(H22)
by (pr0_refl .)
we proved pr0 u0 u0
by (pr0_comp . . previous . . H9 .)
we proved pr0 (THead (Bind Abst) u0 t3) (THead (Bind Abst) u0 t4)
by (H19 . H4 . previous)
arity g c2 (THead (Bind Abst) u0 t4) (AHead a1 a2)
end of H22
(H23)
by (arity_gen_abst . . . . . H22)
ex3_2
A
A
λa1:A.λa2:A.eq A (AHead a1 a2) (AHead a1 a2)
λa1:A.λ:A.arity g c2 u0 (asucc g a1)
λ:A.λa2:A.arity g (CHead c2 (Bind Abst) u0) t4 a2
end of H23
we proceed by induction on H23 to prove arity g c2 (THead (Bind Abbr) v2 t4) a2
case ex3_2_intro : x0:A x1:A H24:eq A (AHead a1 a2) (AHead x0 x1) H25:arity g c2 u0 (asucc g x0) H26:arity g (CHead c2 (Bind Abst) u0) t4 x1 ⇒
the thesis becomes arity g c2 (THead (Bind Abbr) v2 t4) a2
(H27)
by (f_equal . . . . . H24)
we proved
eq
A
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a1 | AHead a0 ⇒a0
<λ:A.A> CASE AHead x0 x1 OF ASort ⇒a1 | AHead a0 ⇒a0
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a1 | AHead a0 ⇒a0 (AHead a1 a2)
λe:A.<λ:A.A> CASE e OF ASort ⇒a1 | AHead a0 ⇒a0 (AHead x0 x1)
end of H27
(h1)
(H28)
by (f_equal . . . . . H24)
we proved
eq
A
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a2 | AHead a0⇒a0
<λ:A.A> CASE AHead x0 x1 OF ASort ⇒a2 | AHead a0⇒a0
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a2 | AHead a0⇒a0 (AHead a1 a2)
λe:A.<λ:A.A> CASE e OF ASort ⇒a2 | AHead a0⇒a0 (AHead x0 x1)
end of H28
suppose H29: eq A a1 x0
(H30)
consider H28
we proved
eq
A
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a2 | AHead a0⇒a0
<λ:A.A> CASE AHead x0 x1 OF ASort ⇒a2 | AHead a0⇒a0
that is equivalent to eq A a2 x1
by (eq_ind_r . . . H26 . previous)
arity g (CHead c2 (Bind Abst) u0) t4 a2
end of H30
(H31)
by (eq_ind_r . . . H25 . H29)
arity g c2 u0 (asucc g a1)
end of H31
by (csuba_refl . .)
we proved csuba g c2 c2
by (csuba_abst . . . previous . . H31 . H21)
we proved csuba g (CHead c2 (Bind Abst) u0) (CHead c2 (Bind Abbr) v2)
by (csuba_arity . . . . H30 . previous)
we proved arity g (CHead c2 (Bind Abbr) v2) t4 a2
by (arity_bind . . not_abbr_abst . . . H21 . . previous)
we proved arity g c2 (THead (Bind Abbr) v2 t4) a2
(eq A a1 x0)→(arity g c2 (THead (Bind Abbr) v2 t4) a2)
end of h1
(h2)
consider H27
we proved
eq
A
<λ:A.A> CASE AHead a1 a2 OF ASort ⇒a1 | AHead a0 ⇒a0
<λ:A.A> CASE AHead x0 x1 OF ASort ⇒a1 | AHead a0 ⇒a0
eq A a1 x0
end of h2
by (h1 h2)
arity g c2 (THead (Bind Abbr) v2 t4) a2
we proved arity g c2 (THead (Bind Abbr) v2 t4) a2
(eq T v1 u)→(arity g c2 (THead (Bind Abbr) v2 t4) a2)
end of h1
(h2)
consider H12
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t3) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Appl) u t OF TSort ⇒v1 | TLRef ⇒v1 | THead t0 ⇒t0
eq T v1 u
end of h2
by (h1 h2)
we proved arity g c2 (THead (Bind Abbr) v2 t4) a2
∀H11:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Flat Appl) u t
.arity g c2 (THead (Bind Abbr) v2 t4) a2
case pr0_upsilon : b:B H7:not (eq B b Abst) v1:T v2:T H8:pr0 v1 v2 u1:T u2:T H10:pr0 u1 u2 t3:T t4:T H12:pr0 t3 t4 ⇒
the thesis becomes
∀H14:eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Flat Appl) u t
.arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2
(H9) by induction hypothesis we know (eq T v1 (THead (Flat Appl) u t))→(arity g c2 v2 a2)
(H11) by induction hypothesis we know (eq T u1 (THead (Flat Appl) u t))→(arity g c2 u2 a2)
(H13) by induction hypothesis we know (eq T t3 (THead (Flat Appl) u t))→(arity g c2 t4 a2)
suppose H14:
eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Flat Appl) u t
(H15)
by (f_equal . . . . . H14)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t3) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Appl) u t OF TSort ⇒v1 | TLRef ⇒v1 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t0 ⇒t0
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒v1 | TLRef ⇒v1 | THead t0 ⇒t0
THead (Flat Appl) u t
end of H15
(h1)
(H16)
by (f_equal . . . . . H14)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t3) OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) u t OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t0⇒t0
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t0⇒t0
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t0⇒t0
THead (Flat Appl) u t
end of H16
suppose H17: eq T v1 u
(H18)
we proceed by induction on H17 to prove (eq T u (THead (Flat Appl) u t))→(arity g c2 v2 a2)
case refl_equal : ⇒
the thesis becomes the hypothesis H9
(eq T u (THead (Flat Appl) u t))→(arity g c2 v2 a2)
end of H18
(H19)
we proceed by induction on H17 to prove pr0 u v2
case refl_equal : ⇒
the thesis becomes the hypothesis H8
pr0 u v2
end of H19
(H23)
consider H16
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t3) OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) u t OF
TSort ⇒THead (Bind b) u1 t3
| TLRef ⇒THead (Bind b) u1 t3
| THead t0⇒t0
that is equivalent to eq T (THead (Bind b) u1 t3) t
by (eq_ind_r . . . H3 . previous)
∀c3:C.(wcpr0 c c3)→∀t5:T.(pr0 (THead (Bind b) u1 t3) t5)→(arity g c3 t5 (AHead a1 a2))
end of H23
(H25) by (H1 . H4 . H19) we proved arity g c2 v2 a1
(H26)
by (pr0_comp . . H10 . . H12 .)
we proved pr0 (THead (Bind b) u1 t3) (THead (Bind b) u2 t4)
by (H23 . H4 . previous)
arity g c2 (THead (Bind b) u2 t4) (AHead a1 a2)
end of H26
(H27)
by (arity_gen_bind . H7 . . . . . H26)
ex2 A λa1:A.arity g c2 u2 a1 λ:A.arity g (CHead c2 (Bind b) u2) t4 (AHead a1 a2)
end of H27
we proceed by induction on H27 to prove
arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2
case ex_intro2 : x:A H28:arity g c2 u2 x H29:arity g (CHead c2 (Bind b) u2) t4 (AHead a1 a2) ⇒
the thesis becomes
arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2
by (drop_refl .)
we proved drop O O c2 c2
that is equivalent to drop (r (Bind b) O) O c2 c2
by (drop_drop . . . . previous .)
we proved drop (S O) O (CHead c2 (Bind b) u2) c2
by (arity_lift . . . . H25 . . . previous)
we proved arity g (CHead c2 (Bind b) u2) (lift (S O) O v2) a1
by (arity_appl . . . . previous . . H29)
we proved
arity
g
CHead c2 (Bind b) u2
THead (Flat Appl) (lift (S O) O v2) t4
a2
by (arity_bind . . H7 . . . H28 . . previous)
arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2
we proved
arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2
eq T v1 u
→(arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2)
end of h1
(h2)
consider H15
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t3) OF
TSort ⇒v1
| TLRef ⇒v1
| THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Appl) u t OF TSort ⇒v1 | TLRef ⇒v1 | THead t0 ⇒t0
eq T v1 u
end of h2
by (h1 h2)
we proved
arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2
∀H14:eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Flat Appl) u t
.arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a2
case pr0_delta : u1:T u2:T :pr0 u1 u2 t3:T t4:T :pr0 t3 t4 w:T :subst0 O u2 t4 w ⇒
the thesis becomes
∀H12:eq T (THead (Bind Abbr) u1 t3) (THead (Flat Appl) u t)
.arity g c2 (THead (Bind Abbr) u2 w) a2
() by induction hypothesis we know (eq T u1 (THead (Flat Appl) u t))→(arity g c2 u2 a2)
() by induction hypothesis we know (eq T t3 (THead (Flat Appl) u t))→(arity g c2 t4 a2)
suppose H12: eq T (THead (Bind Abbr) u1 t3) (THead (Flat Appl) u t)
(H13)
we proceed by induction on H12 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 Abbr) u1 t3 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 Abbr) u1 t3 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 H13
consider H13
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 arity g c2 (THead (Bind Abbr) u2 w) a2
we proved arity g c2 (THead (Bind Abbr) u2 w) a2
∀H12:eq T (THead (Bind Abbr) u1 t3) (THead (Flat Appl) u t)
.arity g c2 (THead (Bind Abbr) u2 w) a2
case pr0_zeta : b:B :not (eq B b Abst) t3:T t4:T :pr0 t3 t4 u0:T ⇒
the thesis becomes
∀H10:eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Flat Appl) u t
.arity g c2 t4 a2
() by induction hypothesis we know (eq T t3 (THead (Flat Appl) u t))→(arity g c2 t4 a2)
suppose H10:
eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Flat Appl) u t
(H11)
we proceed by induction on H10 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 (lift (S O) O t3) 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 (lift (S O) O t3) 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 H11
consider H11
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 arity g c2 t4 a2
we proved arity g c2 t4 a2
∀H10:eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Flat Appl) u t
.arity g c2 t4 a2
case pr0_tau : t3:T t4:T :pr0 t3 t4 u0:T ⇒
the thesis becomes
∀H9:(eq T (THead (Flat Cast) u0 t3) (THead (Flat Appl) u t)).(arity g c2 t4 a2)
() by induction hypothesis we know (eq T t3 (THead (Flat Appl) u t))→(arity g c2 t4 a2)
suppose H9: eq T (THead (Flat Cast) u0 t3) (THead (Flat Appl) u t)
(H10)
we proceed by induction on H9 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 t3 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 t3 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 H10
consider H10
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 arity g c2 t4 a2
we proved arity g c2 t4 a2
∀H9:(eq T (THead (Flat Cast) u0 t3) (THead (Flat Appl) u t)).(arity g c2 t4 a2)
we proved (eq T y (THead (Flat Appl) u t))→(arity g c2 t2 a2)
we proved ∀y:T.(pr0 y t2)→(eq T y (THead (Flat Appl) u t))→(arity g c2 t2 a2)
by (insert_eq . . . . previous H5)
we proved arity g c2 t2 a2
∀c2:C.∀H4:(wcpr0 c c2).∀t2:T.∀H5:(pr0 (THead (Flat Appl) u t) t2).(arity g c2 t2 a2)
case arity_cast : c:C u:T a0:A :arity g c u (asucc g a0) t:T :arity g c t a0 ⇒
the thesis becomes ∀c2:C.∀H4:(wcpr0 c c2).∀t2:T.∀H5:(pr0 (THead (Flat Cast) u t) t2).(arity g c2 t2 a0)
(H1) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t2:T.(pr0 u t2)→(arity g c2 t2 (asucc g a0))
(H3) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t2:T.(pr0 t t2)→(arity g c2 t2 a0)
assume c2: C
suppose H4: wcpr0 c c2
assume t2: T
suppose H5: pr0 (THead (Flat Cast) u t) t2
assume y: T
suppose H6: pr0 y t2
we proceed by induction on H6 to prove (eq T y (THead (Flat Cast) u t))→(arity g c2 t2 a0)
case pr0_refl : t0:T ⇒
the thesis becomes ∀H7:(eq T t0 (THead (Flat Cast) u t)).(arity g c2 t0 a0)
suppose H7: eq T t0 (THead (Flat Cast) u t)
(H8)
by (f_equal . . . . . H7)
we proved eq T t0 (THead (Flat Cast) u t)
eq T (λe:T.e t0) (λe:T.e (THead (Flat Cast) u t))
end of H8
(h1)
by (pr0_refl .)
we proved pr0 u u
by (H1 . H4 . previous)
arity g c2 u (asucc g a0)
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t t
by (H3 . H4 . previous)
arity g c2 t a0
end of h2
by (arity_cast . . . . h1 . h2)
we proved arity g c2 (THead (Flat Cast) u t) a0
by (eq_ind_r . . . previous . H8)
we proved arity g c2 t0 a0
∀H7:(eq T t0 (THead (Flat Cast) u t)).(arity g c2 t0 a0)
case pr0_comp : u1:T u2:T H7:pr0 u1 u2 t3:T t4:T H9:pr0 t3 t4 k:K ⇒
the thesis becomes ∀H11:(eq T (THead k u1 t3) (THead (Flat Cast) u t)).(arity g c2 (THead k u2 t4) a0)
(H8) by induction hypothesis we know (eq T u1 (THead (Flat Cast) u t))→(arity g c2 u2 a0)
(H10) by induction hypothesis we know (eq T t3 (THead (Flat Cast) u t))→(arity g c2 t4 a0)
suppose H11: eq T (THead k u1 t3) (THead (Flat Cast) u t)
(H12)
by (f_equal . . . . . H11)
we proved
eq
K
<λ:T.K> CASE THead k u1 t3 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Flat Cast) u t OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0 (THead k u1 t3)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
THead (Flat Cast) u t
end of H12
(h1)
(H13)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0 (THead k u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
THead (Flat Cast) u t
end of H13
(h1)
(H14)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0 (THead k u1 t3)
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
THead (Flat Cast) u t
end of H14
suppose H15: eq T u1 u
suppose H16: eq K k (Flat Cast)
(H18)
consider H14
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
that is equivalent to eq T t3 t
we proceed by induction on the previous result to prove pr0 t t4
case refl_equal : ⇒
the thesis becomes the hypothesis H9
pr0 t t4
end of H18
(H20)
we proceed by induction on H15 to prove pr0 u u2
case refl_equal : ⇒
the thesis becomes the hypothesis H7
pr0 u u2
end of H20
(h1)
by (H1 . H4 . H20)
arity g c2 u2 (asucc g a0)
end of h1
(h2) by (H3 . H4 . H18) we proved arity g c2 t4 a0
by (arity_cast . . . . h1 . h2)
we proved arity g c2 (THead (Flat Cast) u2 t4) a0
by (eq_ind_r . . . previous . H16)
we proved arity g c2 (THead k u2 t4) a0
(eq T u1 u)→(eq K k (Flat Cast))→(arity g c2 (THead k u2 t4) a0)
end of h1
(h2)
consider H13
we proved
eq
T
<λ:T.T> CASE THead k u1 t3 OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒u1 | TLRef ⇒u1 | THead t0 ⇒t0
eq T u1 u
end of h2
by (h1 h2)
(eq K k (Flat Cast))→(arity g c2 (THead k u2 t4) a0)
end of h1
(h2)
consider H12
we proved
eq
K
<λ:T.K> CASE THead k u1 t3 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Flat Cast) u t OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
eq K k (Flat Cast)
end of h2
by (h1 h2)
we proved arity g c2 (THead k u2 t4) a0
∀H11:(eq T (THead k u1 t3) (THead (Flat Cast) u t)).(arity g c2 (THead k u2 t4) a0)
case pr0_beta : u0:T v1:T v2:T :pr0 v1 v2 t3:T t4:T :pr0 t3 t4 ⇒
the thesis becomes
∀H11:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Flat Cast) u t
.arity g c2 (THead (Bind Abbr) v2 t4) a0
() by induction hypothesis we know (eq T v1 (THead (Flat Cast) u t))→(arity g c2 v2 a0)
() by induction hypothesis we know (eq T t3 (THead (Flat Cast) u t))→(arity g c2 t4 a0)
suppose H11:
eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Flat Cast) u t
(H12)
we proceed by induction on H11 to prove
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t3) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u0 t3) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
end of H12
consider H12
we proved
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
that is equivalent to False
we proceed by induction on the previous result to prove arity g c2 (THead (Bind Abbr) v2 t4) a0
we proved arity g c2 (THead (Bind Abbr) v2 t4) a0
∀H11:eq
T
THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)
THead (Flat Cast) u t
.arity g c2 (THead (Bind Abbr) v2 t4) a0
case pr0_upsilon : b:B :not (eq B b Abst) v1:T v2:T :pr0 v1 v2 u1:T u2:T :pr0 u1 u2 t3:T t4:T :pr0 t3 t4 ⇒
the thesis becomes
∀H14:eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Flat Cast) u t
.arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a0
() by induction hypothesis we know (eq T v1 (THead (Flat Cast) u t))→(arity g c2 v2 a0)
() by induction hypothesis we know (eq T u1 (THead (Flat Cast) u t))→(arity g c2 u2 a0)
() by induction hypothesis we know (eq T t3 (THead (Flat Cast) u t))→(arity g c2 t4 a0)
suppose H14:
eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Flat Cast) u t
(H15)
we proceed by induction on H14 to prove
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t3) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t3) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
end of H15
consider H15
we proved
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a0
we proved
arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a0
∀H14:eq
T
THead (Flat Appl) v1 (THead (Bind b) u1 t3)
THead (Flat Cast) u t
.arity
g
c2
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)
a0
case pr0_delta : u1:T u2:T :pr0 u1 u2 t3:T t4:T :pr0 t3 t4 w:T :subst0 O u2 t4 w ⇒
the thesis becomes
∀H12:eq T (THead (Bind Abbr) u1 t3) (THead (Flat Cast) u t)
.arity g c2 (THead (Bind Abbr) u2 w) a0
() by induction hypothesis we know (eq T u1 (THead (Flat Cast) u t))→(arity g c2 u2 a0)
() by induction hypothesis we know (eq T t3 (THead (Flat Cast) u t))→(arity g c2 t4 a0)
suppose H12: eq T (THead (Bind Abbr) u1 t3) (THead (Flat Cast) u t)
(H13)
we proceed by induction on H12 to prove
<λ:T.Prop>
CASE THead (Flat Cast) 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 Abbr) u1 t3 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 Abbr) u1 t3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
end of H13
consider H13
we proved
<λ:T.Prop>
CASE THead (Flat Cast) 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 arity g c2 (THead (Bind Abbr) u2 w) a0
we proved arity g c2 (THead (Bind Abbr) u2 w) a0
∀H12:eq T (THead (Bind Abbr) u1 t3) (THead (Flat Cast) u t)
.arity g c2 (THead (Bind Abbr) u2 w) a0
case pr0_zeta : b:B :not (eq B b Abst) t3:T t4:T :pr0 t3 t4 u0:T ⇒
the thesis becomes
∀H10:eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Flat Cast) u t
.arity g c2 t4 a0
() by induction hypothesis we know (eq T t3 (THead (Flat Cast) u t))→(arity g c2 t4 a0)
suppose H10:
eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Flat Cast) u t
(H11)
we proceed by induction on H10 to prove
<λ:T.Prop>
CASE THead (Flat Cast) 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 (lift (S O) O t3) 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 (lift (S O) O t3) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
end of H11
consider H11
we proved
<λ:T.Prop>
CASE THead (Flat Cast) 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 arity g c2 t4 a0
we proved arity g c2 t4 a0
∀H10:eq
T
THead (Bind b) u0 (lift (S O) O t3)
THead (Flat Cast) u t
.arity g c2 t4 a0
case pr0_tau : t3:T t4:T H7:pr0 t3 t4 u0:T ⇒
the thesis becomes
∀H9:(eq T (THead (Flat Cast) u0 t3) (THead (Flat Cast) u t)).(arity g c2 t4 a0)
(H8) by induction hypothesis we know (eq T t3 (THead (Flat Cast) u t))→(arity g c2 t4 a0)
suppose H9: eq T (THead (Flat Cast) u0 t3) (THead (Flat Cast) u t)
(H10)
by (f_equal . . . . . H9)
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u0 t3 OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
THead (Flat Cast) u0 t3
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
THead (Flat Cast) u t
end of H10
(h1)
(H11)
by (f_equal . . . . . H9)
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u0 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
THead (Flat Cast) u0 t3
λe:T.<λ:T.T> CASE e OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
THead (Flat Cast) u t
end of H11
suppose : eq T u0 u
(H14)
consider H11
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u0 t3 OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒t3 | TLRef ⇒t3 | THead t0⇒t0
that is equivalent to eq T t3 t
we proceed by induction on the previous result to prove pr0 t t4
case refl_equal : ⇒
the thesis becomes the hypothesis H7
pr0 t t4
end of H14
by (H3 . H4 . H14)
we proved arity g c2 t4 a0
(eq T u0 u)→(arity g c2 t4 a0)
end of h1
(h2)
consider H10
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u0 t3 OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
eq T u0 u
end of h2
by (h1 h2)
we proved arity g c2 t4 a0
∀H9:(eq T (THead (Flat Cast) u0 t3) (THead (Flat Cast) u t)).(arity g c2 t4 a0)
we proved (eq T y (THead (Flat Cast) u t))→(arity g c2 t2 a0)
we proved ∀y:T.(pr0 y t2)→(eq T y (THead (Flat Cast) u t))→(arity g c2 t2 a0)
by (insert_eq . . . . previous H5)
we proved arity g c2 t2 a0
∀c2:C.∀H4:(wcpr0 c c2).∀t2:T.∀H5:(pr0 (THead (Flat Cast) u t) t2).(arity g c2 t2 a0)
case arity_repl : c:C t:T a1:A :arity g c t a1 a2:A H2:leq g a1 a2 ⇒
the thesis becomes ∀c2:C.∀H3:(wcpr0 c c2).∀t2:T.∀H4:(pr0 t t2).(arity g c2 t2 a2)
(H1) by induction hypothesis we know ∀c2:C.(wcpr0 c c2)→∀t2:T.(pr0 t t2)→(arity g c2 t2 a1)
assume c2: C
suppose H3: wcpr0 c c2
assume t2: T
suppose H4: pr0 t t2
by (H1 . H3 . H4)
we proved arity g c2 t2 a1
by (arity_repl . . . . previous . H2)
we proved arity g c2 t2 a2
∀c2:C.∀H3:(wcpr0 c c2).∀t2:T.∀H4:(pr0 t t2).(arity g c2 t2 a2)
we proved ∀c2:C.(wcpr0 c1 c2)→∀t2:T.(pr0 t1 t2)→(arity g c2 t2 a)
we proved ∀g:G.∀c1:C.∀t1:T.∀a:A.(arity g c1 t1 a)→∀c2:C.(wcpr0 c1 c2)→∀t2:T.(pr0 t1 t2)→(arity g c2 t2 a)