DEFINITION arity_appls_abbr()
TYPE =
∀g:G
.∀c:C
.∀d:C
.∀v:T
.∀i:nat
.getl i c (CHead d (Bind Abbr) v)
→∀vs:TList
.∀a:A
.arity g c (THeads (Flat Appl) vs (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) vs (TLRef i)) a
BODY =
assume g: G
assume c: C
assume d: C
assume v: T
assume i: nat
suppose H: getl i c (CHead d (Bind Abbr) v)
assume vs: TList
we proceed by induction on vs to prove
∀a:A
.arity g c (THeads (Flat Appl) vs (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) vs (TLRef i)) a
case TNil : ⇒
the thesis becomes
∀a:A
.arity g c (THeads (Flat Appl) TNil (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) TNil (TLRef i)) a
assume a: A
we must prove
arity g c (THeads (Flat Appl) TNil (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) TNil (TLRef i)) a
or equivalently
arity g c (lift (S i) O v) a
→arity g c (THeads (Flat Appl) TNil (TLRef i)) a
suppose H0: arity g c (lift (S i) O v) a
by (getl_drop . . . . . H)
we proved drop (S i) O c d
by (arity_gen_lift . . . . . . H0 . previous)
we proved arity g d v a
by (arity_abbr . . . . . H . previous)
we proved arity g c (TLRef i) a
that is equivalent to arity g c (THeads (Flat Appl) TNil (TLRef i)) a
we proved
arity g c (lift (S i) O v) a
→arity g c (THeads (Flat Appl) TNil (TLRef i)) a
that is equivalent to
arity g c (THeads (Flat Appl) TNil (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) TNil (TLRef i)) a
∀a:A
.arity g c (THeads (Flat Appl) TNil (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) TNil (TLRef i)) a
case TCons : t:T t0:TList ⇒
the thesis becomes
∀a:A
.arity g c (THeads (Flat Appl) (TCons t t0) (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) (TCons t t0) (TLRef i)) a
(H0) by induction hypothesis we know
∀a:A
.arity g c (THeads (Flat Appl) t0 (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) t0 (TLRef i)) a
assume a: A
we must prove
arity g c (THeads (Flat Appl) (TCons t t0) (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) (TCons t t0) (TLRef i)) a
or equivalently
(arity
g
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O v))
a)
→arity g c (THeads (Flat Appl) (TCons t t0) (TLRef i)) a
suppose H1:
arity
g
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O v))
a
(H2)
by (arity_gen_appl . . . . . H1)
ex2
A
λa1:A.arity g c t a1
λa1:A.arity g c (THeads (Flat Appl) t0 (lift (S i) O v)) (AHead a1 a)
end of H2
we proceed by induction on H2 to prove
arity
g
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
a
case ex_intro2 : x:A H3:arity g c t x H4:arity g c (THeads (Flat Appl) t0 (lift (S i) O v)) (AHead x a) ⇒
the thesis becomes
arity
g
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
a
by (H0 . H4)
we proved arity g c (THeads (Flat Appl) t0 (TLRef i)) (AHead x a)
by (arity_appl . . . . H3 . . previous)
arity
g
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
a
we proved
arity
g
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
a
that is equivalent to arity g c (THeads (Flat Appl) (TCons t t0) (TLRef i)) a
we proved
(arity
g
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O v))
a)
→arity g c (THeads (Flat Appl) (TCons t t0) (TLRef i)) a
that is equivalent to
arity g c (THeads (Flat Appl) (TCons t t0) (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) (TCons t t0) (TLRef i)) a
∀a:A
.arity g c (THeads (Flat Appl) (TCons t t0) (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) (TCons t t0) (TLRef i)) a
we proved
∀a:A
.arity g c (THeads (Flat Appl) vs (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) vs (TLRef i)) a
we proved
∀g:G
.∀c:C
.∀d:C
.∀v:T
.∀i:nat
.getl i c (CHead d (Bind Abbr) v)
→∀vs:TList
.∀a:A
.arity g c (THeads (Flat Appl) vs (lift (S i) O v)) a
→arity g c (THeads (Flat Appl) vs (TLRef i)) a