DEFINITION arity_mono()
TYPE =
∀g:G.∀c:C.∀t:T.∀a1:A.(arity g c t a1)→∀a2:A.(arity g c t a2)→(leq g a1 a2)
BODY =
assume g: G
assume c: C
assume t: T
assume a1: A
suppose H: arity g c t a1
we proceed by induction on H to prove ∀a2:A.(arity g c t a2)→(leq g a1 a2)
case arity_sort : c0:C n:nat ⇒
the thesis becomes ∀a2:A.∀H0:(arity g c0 (TSort n) a2).(leq g (ASort O n) a2)
assume a2: A
suppose H0: arity g c0 (TSort n) a2
by (arity_gen_sort . . . . H0)
we proved leq g a2 (ASort O n)
by (leq_sym . . . previous)
we proved leq g (ASort O n) a2
∀a2:A.∀H0:(arity g c0 (TSort n) a2).(leq g (ASort O n) a2)
case arity_abbr : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u) a:A :arity g d u a ⇒
the thesis becomes ∀a2:A.∀H3:(arity g c0 (TLRef i) a2).(leq g a a2)
(H2) by induction hypothesis we know ∀a2:A.(arity g d u a2)→(leq g a a2)
assume a2: A
suppose H3: arity g c0 (TLRef i) a2
(H4)
by (arity_gen_lref . . . . H3)
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
end of H4
we proceed by induction on H4 to prove leq g a a2
case or_introl : H5:ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abbr) u0) λd0:C.λu0:T.arity g d0 u0 a2 ⇒
the thesis becomes leq g a a2
we proceed by induction on H5 to prove leq g a a2
case ex2_2_intro : x0:C x1:T H6:getl i c0 (CHead x0 (Bind Abbr) x1) H7:arity g x0 x1 a2 ⇒
the thesis becomes leq g a a2
(H8)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abbr) u) (CHead x0 (Bind Abbr) x1)
we proceed by induction on the previous result to prove getl i c0 (CHead x0 (Bind Abbr) x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl i c0 (CHead x0 (Bind Abbr) x1)
end of H8
(H9)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abbr) u) (CHead x0 (Bind Abbr) x1)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒d | CHead c1 ⇒c1
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead d (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead x0 (Bind Abbr) x1)
end of H9
(h1)
(H10)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abbr) u) (CHead x0 (Bind Abbr) x1)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒u | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead d (Bind Abbr) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead x0 (Bind Abbr) x1)
end of H10
suppose H11: eq C d x0
(H12)
consider H10
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u x1
by (eq_ind_r . . . H8 . previous)
getl i c0 (CHead x0 (Bind Abbr) u)
end of H12
(H13)
consider H10
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u x1
by (eq_ind_r . . . H7 . previous)
arity g x0 u a2
end of H13
(H15)
by (eq_ind_r . . . H13 . H11)
arity g d u a2
end of H15
by (H2 . H15)
we proved leq g a a2
(eq C d x0)→(leq g a a2)
end of h1
(h2)
consider H9
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒d | CHead c1 ⇒c1
eq C d x0
end of h2
by (h1 h2)
leq g a a2
leq g a a2
case or_intror : H5:ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abst) u0) λd0:C.λu0:T.arity g d0 u0 (asucc g a2) ⇒
the thesis becomes leq g a a2
we proceed by induction on H5 to prove leq g a a2
case ex2_2_intro : x0:C x1:T H6:getl i c0 (CHead x0 (Bind Abst) x1) :arity g x0 x1 (asucc g a2) ⇒
the thesis becomes leq g a a2
(H9)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abbr) u) (CHead x0 (Bind Abst) x1)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead x0 (Bind Abst) x1 OF
CSort ⇒False
| CHead 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
<λ:C.Prop>
CASE CHead d (Bind Abbr) u OF
CSort ⇒False
| CHead 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
<λ:C.Prop>
CASE CHead d (Bind Abbr) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead x0 (Bind Abst) x1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
end of H9
consider H9
we proved
<λ:C.Prop>
CASE CHead x0 (Bind Abst) x1 OF
CSort ⇒False
| CHead 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 leq g a a2
leq g a a2
leq g a a2
we proved leq g a a2
∀a2:A.∀H3:(arity g c0 (TLRef i) a2).(leq g a a2)
case arity_abst : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abst) u) a:A :arity g d u (asucc g a) ⇒
the thesis becomes ∀a2:A.∀H3:(arity g c0 (TLRef i) a2).(leq g a a2)
(H2) by induction hypothesis we know ∀a2:A.(arity g d u a2)→(leq g (asucc g a) a2)
assume a2: A
suppose H3: arity g c0 (TLRef i) a2
(H4)
by (arity_gen_lref . . . . H3)
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
end of H4
we proceed by induction on H4 to prove leq g a a2
case or_introl : H5:ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abbr) u0) λd0:C.λu0:T.arity g d0 u0 a2 ⇒
the thesis becomes leq g a a2
we proceed by induction on H5 to prove leq g a a2
case ex2_2_intro : x0:C x1:T H6:getl i c0 (CHead x0 (Bind Abbr) x1) :arity g x0 x1 a2 ⇒
the thesis becomes leq g a a2
(H9)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abst) u) (CHead x0 (Bind Abbr) x1)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead x0 (Bind Abbr) x1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead x0 (Bind Abbr) x1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H9
consider H9
we proved
<λ:C.Prop>
CASE CHead x0 (Bind Abbr) x1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove leq g a a2
leq g a a2
leq g a a2
case or_intror : H5:ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abst) u0) λd0:C.λu0:T.arity g d0 u0 (asucc g a2) ⇒
the thesis becomes leq g a a2
we proceed by induction on H5 to prove leq g a a2
case ex2_2_intro : x0:C x1:T H6:getl i c0 (CHead x0 (Bind Abst) x1) H7:arity g x0 x1 (asucc g a2) ⇒
the thesis becomes leq g a a2
(H8)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abst) u) (CHead x0 (Bind Abst) x1)
we proceed by induction on the previous result to prove getl i c0 (CHead x0 (Bind Abst) x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl i c0 (CHead x0 (Bind Abst) x1)
end of H8
(H9)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abst) u) (CHead x0 (Bind Abst) x1)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead x0 (Bind Abst) x1 OF CSort ⇒d | CHead c1 ⇒c1
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead d (Bind Abst) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead x0 (Bind Abst) x1)
end of H9
(h1)
(H10)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abst) u) (CHead x0 (Bind Abst) x1)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abst) x1 OF CSort ⇒u | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead d (Bind Abst) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead x0 (Bind Abst) x1)
end of H10
suppose H11: eq C d x0
(H12)
consider H10
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abst) x1 OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u x1
by (eq_ind_r . . . H8 . previous)
getl i c0 (CHead x0 (Bind Abst) u)
end of H12
(H13)
consider H10
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abst) x1 OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u x1
by (eq_ind_r . . . H7 . previous)
arity g x0 u (asucc g a2)
end of H13
(H15)
by (eq_ind_r . . . H13 . H11)
arity g d u (asucc g a2)
end of H15
by (H2 . H15)
we proved leq g (asucc g a) (asucc g a2)
by (asucc_inj . . . previous)
we proved leq g a a2
(eq C d x0)→(leq g a a2)
end of h1
(h2)
consider H9
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead x0 (Bind Abst) x1 OF CSort ⇒d | CHead c1 ⇒c1
eq C d x0
end of h2
by (h1 h2)
leq g a a2
leq g a a2
we proved leq g a a2
∀a2:A.∀H3:(arity g c0 (TLRef i) a2).(leq g a a2)
case arity_bind : b:B H0:not (eq B b Abst) c0:C u:T a2:A :arity g c0 u a2 t0:T a3:A :arity g (CHead c0 (Bind b) u) t0 a3 ⇒
the thesis becomes ∀a0:A.∀H5:(arity g c0 (THead (Bind b) u t0) a0).(leq g a3 a0)
() by induction hypothesis we know ∀a3:A.(arity g c0 u a3)→(leq g a2 a3)
(H4) by induction hypothesis we know ∀a4:A.(arity g (CHead c0 (Bind b) u) t0 a4)→(leq g a3 a4)
assume a0: A
suppose H5: arity g c0 (THead (Bind b) u t0) a0
(H6)
by (arity_gen_bind . H0 . . . . . H5)
ex2 A λa1:A.arity g c0 u a1 λ:A.arity g (CHead c0 (Bind b) u) t0 a0
end of H6
we proceed by induction on H6 to prove leq g a3 a0
case ex_intro2 : x:A :arity g c0 u x H8:arity g (CHead c0 (Bind b) u) t0 a0 ⇒
the thesis becomes leq g a3 a0
by (H4 . H8)
leq g a3 a0
we proved leq g a3 a0
∀a0:A.∀H5:(arity g c0 (THead (Bind b) u t0) a0).(leq g a3 a0)
case arity_head : c0:C u:T a2:A :arity g c0 u (asucc g a2) t0:T a3:A :arity g (CHead c0 (Bind Abst) u) t0 a3 ⇒
the thesis becomes ∀a0:A.∀H4:(arity g c0 (THead (Bind Abst) u t0) a0).(leq g (AHead a2 a3) a0)
(H1) by induction hypothesis we know ∀a3:A.(arity g c0 u a3)→(leq g (asucc g a2) a3)
(H3) by induction hypothesis we know ∀a4:A.(arity g (CHead c0 (Bind Abst) u) t0 a4)→(leq g a3 a4)
assume a0: A
suppose H4: arity g c0 (THead (Bind Abst) u t0) a0
(H5)
by (arity_gen_abst . . . . . H4)
ex3_2
A
A
λa1:A.λa2:A.eq A a0 (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t0 a2
end of H5
we proceed by induction on H5 to prove leq g (AHead a2 a3) a0
case ex3_2_intro : x0:A x1:A H6:eq A a0 (AHead x0 x1) H7:arity g c0 u (asucc g x0) H8:arity g (CHead c0 (Bind Abst) u) t0 x1 ⇒
the thesis becomes leq g (AHead a2 a3) a0
(h1)
by (H1 . H7)
we proved leq g (asucc g a2) (asucc g x0)
by (asucc_inj . . . previous)
leq g a2 x0
end of h1
(h2) by (H3 . H8) we proved leq g a3 x1
by (leq_head . . . h1 . . h2)
we proved leq g (AHead a2 a3) (AHead x0 x1)
by (eq_ind_r . . . previous . H6)
leq g (AHead a2 a3) a0
we proved leq g (AHead a2 a3) a0
∀a0:A.∀H4:(arity g c0 (THead (Bind Abst) u t0) a0).(leq g (AHead a2 a3) a0)
case arity_appl : c0:C u:T a2:A :arity g c0 u a2 t0:T a3:A :arity g c0 t0 (AHead a2 a3) ⇒
the thesis becomes ∀a0:A.∀H4:(arity g c0 (THead (Flat Appl) u t0) a0).(leq g a3 a0)
() by induction hypothesis we know ∀a3:A.(arity g c0 u a3)→(leq g a2 a3)
(H3) by induction hypothesis we know ∀a4:A.(arity g c0 t0 a4)→(leq g (AHead a2 a3) a4)
assume a0: A
suppose H4: arity g c0 (THead (Flat Appl) u t0) a0
(H5)
by (arity_gen_appl . . . . . H4)
ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t0 (AHead a1 a0)
end of H5
we proceed by induction on H5 to prove leq g a3 a0
case ex_intro2 : x:A :arity g c0 u x H7:arity g c0 t0 (AHead x a0) ⇒
the thesis becomes leq g a3 a0
by (H3 . H7)
we proved leq g (AHead a2 a3) (AHead x a0)
by (ahead_inj_snd . . . . . previous)
leq g a3 a0
we proved leq g a3 a0
∀a0:A.∀H4:(arity g c0 (THead (Flat Appl) u t0) a0).(leq g a3 a0)
case arity_cast : c0:C u:T a:A :arity g c0 u (asucc g a) t0:T :arity g c0 t0 a ⇒
the thesis becomes ∀a2:A.∀H4:(arity g c0 (THead (Flat Cast) u t0) a2).(leq g a a2)
() by induction hypothesis we know ∀a2:A.(arity g c0 u a2)→(leq g (asucc g a) a2)
(H3) by induction hypothesis we know ∀a2:A.(arity g c0 t0 a2)→(leq g a a2)
assume a2: A
suppose H4: arity g c0 (THead (Flat Cast) u t0) a2
(H5)
by (arity_gen_cast . . . . . H4)
land (arity g c0 u (asucc g a2)) (arity g c0 t0 a2)
end of H5
we proceed by induction on H5 to prove leq g a a2
case conj : :arity g c0 u (asucc g a2) H7:arity g c0 t0 a2 ⇒
the thesis becomes leq g a a2
by (H3 . H7)
leq g a a2
we proved leq g a a2
∀a2:A.∀H4:(arity g c0 (THead (Flat Cast) u t0) a2).(leq g a a2)
case arity_repl : c0:C t0:T a2:A :arity g c0 t0 a2 a3:A H2:leq g a2 a3 ⇒
the thesis becomes ∀a0:A.∀H3:(arity g c0 t0 a0).(leq g a3 a0)
(H1) by induction hypothesis we know ∀a3:A.(arity g c0 t0 a3)→(leq g a2 a3)
assume a0: A
suppose H3: arity g c0 t0 a0
(h1)
by (leq_sym . . . H2)
leq g a3 a2
end of h1
(h2) by (H1 . H3) we proved leq g a2 a0
by (leq_trans . . . h1 . h2)
we proved leq g a3 a0
∀a0:A.∀H3:(arity g c0 t0 a0).(leq g a3 a0)
we proved ∀a2:A.(arity g c t a2)→(leq g a1 a2)
we proved ∀g:G.∀c:C.∀t:T.∀a1:A.(arity g c t a1)→∀a2:A.(arity g c t a2)→(leq g a1 a2)