DEFINITION csuba_arity_rev()
TYPE =
∀g:G
.∀c1:C
.∀t:T
.∀a:A
.(arity g c1 t a)→∀c2:C.(csuba g c2 c1)→(csubv c2 c1)→(arity g c2 t a)
BODY =
assume g: G
assume c1: C
assume t: T
assume a: A
suppose H: arity g c1 t a
we proceed by induction on H to prove ∀c2:C.(csuba g c2 c1)→(csubv c2 c1)→(arity g c2 t a)
case arity_sort : c:C n:nat ⇒
the thesis becomes
∀c2:C
.csuba g c2 c
→(csubv c2 c)→(arity g c2 (TSort n) (ASort O n))
assume c2: C
suppose : csuba g c2 c
suppose : csubv c2 c
by (arity_sort . . .)
we proved arity g c2 (TSort n) (ASort O n)
∀c2:C
.csuba g c2 c
→(csubv c2 c)→(arity g c2 (TSort n) (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 H1:arity g d u a0 ⇒
the thesis becomes ∀c2:C.∀H3:(csuba g c2 c).∀H4:(csubv c2 c).(arity g c2 (TLRef i) a0)
(H2) by induction hypothesis we know ∀c2:C.(csuba g c2 d)→(csubv c2 d)→(arity g c2 u a0)
assume c2: C
suppose H3: csuba g c2 c
suppose H4: csubv c2 c
(H_x)
by (csuba_getl_abbr_rev . . . . . H0 . H3)
or3
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d2 d
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 d
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g d u a
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove arity g c2 (TLRef i) a0
case or3_intro0 : H6:ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d2 d ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H6 to prove arity g c2 (TLRef i) a0
case ex_intro2 : x:C H7:getl i c2 (CHead x (Bind Abbr) u) H8:csuba g x d ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H_x0)
by (csubv_getl_conf . . H4 . . . . H7)
ex2_3 B C T λ:B.λd2:C.λ:T.csubv x d2 λb2:B.λd2:C.λv2:T.getl i c (CHead d2 (Bind b2) v2)
end of H_x0
(H9) consider H_x0
we proceed by induction on H9 to prove arity g c2 (TLRef i) a0
case ex2_3_intro : x0:B x1:C x2:T H10:csubv x x1 H11:getl i c (CHead x1 (Bind x0) x2) ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H12)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2)
we proceed by induction on the previous result to prove getl i c (CHead x1 (Bind x0) x2)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl i c (CHead x1 (Bind x0) x2)
end of H12
(H13)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x2)
end of H13
(h1)
(H14)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead d (Bind Abbr) u
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
CHead x1 (Bind x0) x2
end of H14
(h1)
(H15)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2)
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 x1 (Bind x0) x2 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 x1 (Bind x0) x2)
end of H15
suppose H16: eq B Abbr x0
suppose H17: eq C d x1
(H18)
consider H15
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u x2
by (eq_ind_r . . . H12 . previous)
getl i c (CHead x1 (Bind x0) u)
end of H18
(H19)
by (eq_ind_r . . . H18 . H17)
getl i c (CHead d (Bind x0) u)
end of H19
(H20)
by (eq_ind_r . . . H10 . H17)
csubv x d
end of H20
by (H2 . H8 H20)
we proved arity g x u a0
by (arity_abbr . . . . . H7 . previous)
we proved arity g c2 (TLRef i) a0
(eq B Abbr x0)→(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H14
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abbr
eq B Abbr x0
end of h2
by (h1 h2)
(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H13
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
case or3_intro1 : H6:ex4_3 C T A λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abst) u2) λd2:C.λ:T.λ:A.csuba g d2 d λd2:C.λu2:T.λa1:A.arity g d2 u2 (asucc g a1) λ:C.λ:T.λa1:A.arity g d u a1 ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H6 to prove arity g c2 (TLRef i) a0
case ex4_3_intro : x0:C x1:T x2:A H7:getl i c2 (CHead x0 (Bind Abst) x1) :csuba g x0 d H9:arity g x0 x1 (asucc g x2) H10:arity g d u x2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
(h1)
by (arity_abst . . . . . H7 . H9)
arity g c2 (TLRef i) x2
end of h1
(h2)
by (arity_mono . . . . H10 . H1)
leq g x2 a0
end of h2
by (arity_repl . . . . h1 . h2)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
case or3_intro2 : H6:ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H6 to prove arity g c2 (TLRef i) a0
case ex2_2_intro : x0:C x1:T H7:getl i c2 (CHead x0 (Bind Void) x1) :csuba g x0 d ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H_x0)
by (csubv_getl_conf_void . . H4 . . . H7)
ex2_2 C T λd2:C.λ:T.csubv x0 d2 λd2:C.λv2:T.getl i c (CHead d2 (Bind Void) v2)
end of H_x0
(H9) consider H_x0
we proceed by induction on H9 to prove arity g c2 (TLRef i) a0
case ex2_2_intro : x2:C x3:T :csubv x0 x2 H11:getl i c (CHead x2 (Bind Void) x3) ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H13)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abbr) u) (CHead x2 (Bind Void) x3)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead x2 (Bind Void) x3 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 x2 (Bind Void) x3 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 H13
consider H13
we proved
<λ:C.Prop>
CASE CHead x2 (Bind Void) x3 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 arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
we proved arity g c2 (TLRef i) a0
∀c2:C.∀H3:(csuba g c2 c).∀H4:(csubv c2 c).(arity g c2 (TLRef i) 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:(csuba g c2 c).∀H4:(csubv c2 c).(arity g c2 (TLRef i) a0)
(H2) by induction hypothesis we know ∀c2:C.(csuba g c2 d)→(csubv c2 d)→(arity g c2 u (asucc g a0))
assume c2: C
suppose H3: csuba g c2 c
suppose H4: csubv c2 c
(H_x)
by (csuba_getl_abst_rev . . . . . H0 . H3)
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d
ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove arity g c2 (TLRef i) a0
case or_introl : H6:ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H6 to prove arity g c2 (TLRef i) a0
case ex_intro2 : x:C H7:getl i c2 (CHead x (Bind Abst) u) H8:csuba g x d ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H_x0)
by (csubv_getl_conf . . H4 . . . . H7)
ex2_3 B C T λ:B.λd2:C.λ:T.csubv x d2 λb2:B.λd2:C.λv2:T.getl i c (CHead d2 (Bind b2) v2)
end of H_x0
(H9) consider H_x0
we proceed by induction on H9 to prove arity g c2 (TLRef i) a0
case ex2_3_intro : x0:B x1:C x2:T H10:csubv x x1 H11:getl i c (CHead x1 (Bind x0) x2) ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H12)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x2)
we proceed by induction on the previous result to prove getl i c (CHead x1 (Bind x0) x2)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl i c (CHead x1 (Bind x0) x2)
end of H12
(H13)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x2)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abst) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead x1 (Bind x0) x2)
end of H13
(h1)
(H14)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x2)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead d (Bind Abst) u
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
CHead x1 (Bind x0) x2
end of H14
(h1)
(H15)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x2)
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 x1 (Bind x0) x2 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 x1 (Bind x0) x2)
end of H15
suppose H16: eq B Abst x0
suppose H17: eq C d x1
(H18)
consider H15
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead x1 (Bind x0) x2 OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u x2
by (eq_ind_r . . . H12 . previous)
getl i c (CHead x1 (Bind x0) u)
end of H18
(H19)
by (eq_ind_r . . . H18 . H17)
getl i c (CHead d (Bind x0) u)
end of H19
(H20)
by (eq_ind_r . . . H10 . H17)
csubv x d
end of H20
by (H2 . H8 H20)
we proved arity g x u (asucc g a0)
by (arity_abst . . . . . H7 . previous)
we proved arity g c2 (TLRef i) a0
(eq B Abst x0)→(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H14
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abst) u OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:C.B>
CASE CHead x1 (Bind x0) x2 OF
CSort ⇒Abst
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq B Abst x0
end of h2
by (h1 h2)
(eq C d x1)→(arity g c2 (TLRef i) a0)
end of h1
(h2)
consider H13
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x1 (Bind x0) x2 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x1
end of h2
by (h1 h2)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
case or_intror : H6:ex2_2 C T λd2:C.λu2:T.getl i c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H6 to prove arity g c2 (TLRef i) a0
case ex2_2_intro : x0:C x1:T H7:getl i c2 (CHead x0 (Bind Void) x1) :csuba g x0 d ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H_x0)
by (csubv_getl_conf_void . . H4 . . . H7)
ex2_2 C T λd2:C.λ:T.csubv x0 d2 λd2:C.λv2:T.getl i c (CHead d2 (Bind Void) v2)
end of H_x0
(H9) consider H_x0
we proceed by induction on H9 to prove arity g c2 (TLRef i) a0
case ex2_2_intro : x2:C x3:T :csubv x0 x2 H11:getl i c (CHead x2 (Bind Void) x3) ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H13)
by (getl_mono . . . H0 . H11)
we proved eq C (CHead d (Bind Abst) u) (CHead x2 (Bind Void) x3)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead x2 (Bind Void) x3 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 x2 (Bind Void) x3 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 H13
consider H13
we proved
<λ:C.Prop>
CASE CHead x2 (Bind Void) x3 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 arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
we proved arity g c2 (TLRef i) a0
∀c2:C.∀H3:(csuba g c2 c).∀H4:(csubv c2 c).(arity g c2 (TLRef i) a0)
case arity_bind : b:B H0:not (eq B b Abst) c:C u:T a1:A :arity g c u a1 t0:T a2:A :arity g (CHead c (Bind b) u) t0 a2 ⇒
the thesis becomes ∀c2:C.∀H5:(csuba g c2 c).∀H6:(csubv c2 c).(arity g c2 (THead (Bind b) u t0) a2)
(H2) by induction hypothesis we know ∀c2:C.(csuba g c2 c)→(csubv c2 c)→(arity g c2 u a1)
(H4) by induction hypothesis we know
∀c2:C
.csuba g c2 (CHead c (Bind b) u)
→(csubv c2 (CHead c (Bind b) u))→(arity g c2 t0 a2)
assume c2: C
suppose H5: csuba g c2 c
suppose H6: csubv c2 c
(h1) by (H2 . H5 H6) we proved arity g c2 u a1
(h2)
(h1)
by (csuba_head . . . H5 . .)
csuba g (CHead c2 (Bind b) u) (CHead c (Bind b) u)
end of h1
(h2)
by (csubv_bind_same . . H6 . . .)
csubv (CHead c2 (Bind b) u) (CHead c (Bind b) u)
end of h2
by (H4 . h1 h2)
arity g (CHead c2 (Bind b) u) t0 a2
end of h2
by (arity_bind . . H0 . . . h1 . . h2)
we proved arity g c2 (THead (Bind b) u t0) a2
∀c2:C.∀H5:(csuba g c2 c).∀H6:(csubv c2 c).(arity g c2 (THead (Bind b) u t0) a2)
case arity_head : c:C u:T a1:A :arity g c u (asucc g a1) t0:T a2:A :arity g (CHead c (Bind Abst) u) t0 a2 ⇒
the thesis becomes
∀c2:C
.∀H4:csuba g c2 c
.∀H5:(csubv c2 c).(arity g c2 (THead (Bind Abst) u t0) (AHead a1 a2))
(H1) by induction hypothesis we know ∀c2:C.(csuba g c2 c)→(csubv c2 c)→(arity g c2 u (asucc g a1))
(H3) by induction hypothesis we know
∀c2:C
.csuba g c2 (CHead c (Bind Abst) u)
→(csubv c2 (CHead c (Bind Abst) u))→(arity g c2 t0 a2)
assume c2: C
suppose H4: csuba g c2 c
suppose H5: csubv c2 c
(h1)
by (H1 . H4 H5)
arity g c2 u (asucc g a1)
end of h1
(h2)
(h1)
by (csuba_head . . . H4 . .)
csuba g (CHead c2 (Bind Abst) u) (CHead c (Bind Abst) u)
end of h1
(h2)
by (csubv_bind_same . . H5 . . .)
csubv (CHead c2 (Bind Abst) u) (CHead c (Bind Abst) u)
end of h2
by (H3 . h1 h2)
arity g (CHead c2 (Bind Abst) u) t0 a2
end of h2
by (arity_head . . . . h1 . . h2)
we proved arity g c2 (THead (Bind Abst) u t0) (AHead a1 a2)
∀c2:C
.∀H4:csuba g c2 c
.∀H5:(csubv c2 c).(arity g c2 (THead (Bind Abst) u t0) (AHead a1 a2))
case arity_appl : c:C u:T a1:A :arity g c u a1 t0:T a2:A :arity g c t0 (AHead a1 a2) ⇒
the thesis becomes ∀c2:C.∀H4:(csuba g c2 c).∀H5:(csubv c2 c).(arity g c2 (THead (Flat Appl) u t0) a2)
(H1) by induction hypothesis we know ∀c2:C.(csuba g c2 c)→(csubv c2 c)→(arity g c2 u a1)
(H3) by induction hypothesis we know ∀c2:C.(csuba g c2 c)→(csubv c2 c)→(arity g c2 t0 (AHead a1 a2))
assume c2: C
suppose H4: csuba g c2 c
suppose H5: csubv c2 c
(h1) by (H1 . H4 H5) we proved arity g c2 u a1
(h2)
by (H3 . H4 H5)
arity g c2 t0 (AHead a1 a2)
end of h2
by (arity_appl . . . . h1 . . h2)
we proved arity g c2 (THead (Flat Appl) u t0) a2
∀c2:C.∀H4:(csuba g c2 c).∀H5:(csubv c2 c).(arity g c2 (THead (Flat Appl) u t0) a2)
case arity_cast : c:C u:T a0:A :arity g c u (asucc g a0) t0:T :arity g c t0 a0 ⇒
the thesis becomes ∀c2:C.∀H4:(csuba g c2 c).∀H5:(csubv c2 c).(arity g c2 (THead (Flat Cast) u t0) a0)
(H1) by induction hypothesis we know ∀c2:C.(csuba g c2 c)→(csubv c2 c)→(arity g c2 u (asucc g a0))
(H3) by induction hypothesis we know ∀c2:C.(csuba g c2 c)→(csubv c2 c)→(arity g c2 t0 a0)
assume c2: C
suppose H4: csuba g c2 c
suppose H5: csubv c2 c
(h1)
by (H1 . H4 H5)
arity g c2 u (asucc g a0)
end of h1
(h2) by (H3 . H4 H5) we proved arity g c2 t0 a0
by (arity_cast . . . . h1 . h2)
we proved arity g c2 (THead (Flat Cast) u t0) a0
∀c2:C.∀H4:(csuba g c2 c).∀H5:(csubv c2 c).(arity g c2 (THead (Flat Cast) u t0) a0)
case arity_repl : c:C t0:T a1:A :arity g c t0 a1 a2:A H2:leq g a1 a2 ⇒
the thesis becomes ∀c2:C.∀H3:(csuba g c2 c).∀H4:(csubv c2 c).(arity g c2 t0 a2)
(H1) by induction hypothesis we know ∀c2:C.(csuba g c2 c)→(csubv c2 c)→(arity g c2 t0 a1)
assume c2: C
suppose H3: csuba g c2 c
suppose H4: csubv c2 c
by (H1 . H3 H4)
we proved arity g c2 t0 a1
by (arity_repl . . . . previous . H2)
we proved arity g c2 t0 a2
∀c2:C.∀H3:(csuba g c2 c).∀H4:(csubv c2 c).(arity g c2 t0 a2)
we proved ∀c2:C.(csuba g c2 c1)→(csubv c2 c1)→(arity g c2 t a)
we proved
∀g:G
.∀c1:C
.∀t:T
.∀a:A
.(arity g c1 t a)→∀c2:C.(csuba g c2 c1)→(csubv c2 c1)→(arity g c2 t a)