DEFINITION arity_appls_bind()
TYPE =
∀g:G
.∀b:B
.not (eq B b Abst)
→∀c:C
.∀v:T
.∀a1:A
.arity g c v a1
→∀t:T
.∀vs:TList
.∀a2:A
.(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t
a2)
→arity g c (THeads (Flat Appl) vs (THead (Bind b) v t)) a2
BODY =
assume g: G
assume b: B
suppose H: not (eq B b Abst)
assume c: C
assume v: T
assume a1: A
suppose H0: arity g c v a1
assume t: T
assume vs: TList
we proceed by induction on vs to prove
∀a2:A
.(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t
a2)
→arity g c (THeads (Flat Appl) vs (THead (Bind b) v t)) a2
case TNil : ⇒
the thesis becomes
∀a2:A
.(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O TNil) t
a2)
→arity g c (THeads (Flat Appl) TNil (THead (Bind b) v t)) a2
assume a2: A
we must prove
(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O TNil) t
a2)
→arity g c (THeads (Flat Appl) TNil (THead (Bind b) v t)) a2
or equivalently
arity g (CHead c (Bind b) v) t a2
→arity g c (THeads (Flat Appl) TNil (THead (Bind b) v t)) a2
suppose H1: arity g (CHead c (Bind b) v) t a2
by (arity_bind . . H . . . H0 . . H1)
we proved arity g c (THead (Bind b) v t) a2
that is equivalent to arity g c (THeads (Flat Appl) TNil (THead (Bind b) v t)) a2
we proved
arity g (CHead c (Bind b) v) t a2
→arity g c (THeads (Flat Appl) TNil (THead (Bind b) v t)) a2
that is equivalent to
(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O TNil) t
a2)
→arity g c (THeads (Flat Appl) TNil (THead (Bind b) v t)) a2
∀a2:A
.(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O TNil) t
a2)
→arity g c (THeads (Flat Appl) TNil (THead (Bind b) v t)) a2
case TCons : t0:T t1:TList ⇒
the thesis becomes
∀a2:A
.(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O (TCons t0 t1)) t
a2)
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Bind b) v t)
a2)
(H1) by induction hypothesis we know
∀a2:A
.(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O t1) t
a2)
→arity g c (THeads (Flat Appl) t1 (THead (Bind b) v t)) a2
assume a2: A
we must prove
(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O (TCons t0 t1)) t
a2)
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Bind b) v t)
a2)
or equivalently
(arity
g
CHead c (Bind b) v
THead
Flat Appl
lift (S O) O t0
THeads (Flat Appl) (lifts (S O) O t1) t
a2)
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Bind b) v t)
a2)
suppose H2:
arity
g
CHead c (Bind b) v
THead
Flat Appl
lift (S O) O t0
THeads (Flat Appl) (lifts (S O) O t1) t
a2
(H3)
by (arity_gen_appl . . . . . H2)
ex2
A
λa1:A.arity g (CHead c (Bind b) v) (lift (S O) O t0) a1
λa1:A
.arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O t1) t
AHead a1 a2
end of H3
we proceed by induction on H3 to prove
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Bind b) v t)
a2
case ex_intro2 : x:A H4:arity g (CHead c (Bind b) v) (lift (S O) O t0) x H5:arity g (CHead c (Bind b) v) (THeads (Flat Appl) (lifts (S O) O t1) t) (AHead x a2) ⇒
the thesis becomes
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Bind b) v t)
a2
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
we proved drop (S O) O (CHead c (Bind b) v) c
by (arity_gen_lift . . . . . . H4 . previous)
arity g c t0 x
end of h1
(h2)
by (H1 . H5)
arity
g
c
THeads (Flat Appl) t1 (THead (Bind b) v t)
AHead x a2
end of h2
by (arity_appl . . . . h1 . . h2)
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Bind b) v t)
a2
we proved
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Bind b) v t)
a2
that is equivalent to
arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Bind b) v t)
a2
we proved
(arity
g
CHead c (Bind b) v
THead
Flat Appl
lift (S O) O t0
THeads (Flat Appl) (lifts (S O) O t1) t
a2)
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Bind b) v t)
a2)
that is equivalent to
(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O (TCons t0 t1)) t
a2)
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Bind b) v t)
a2)
∀a2:A
.(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O (TCons t0 t1)) t
a2)
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Bind b) v t)
a2)
we proved
∀a2:A
.(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t
a2)
→arity g c (THeads (Flat Appl) vs (THead (Bind b) v t)) a2
we proved
∀g:G
.∀b:B
.not (eq B b Abst)
→∀c:C
.∀v:T
.∀a1:A
.arity g c v a1
→∀t:T
.∀vs:TList
.∀a2:A
.(arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t
a2)
→arity g c (THeads (Flat Appl) vs (THead (Bind b) v t)) a2