DEFINITION sn3_appls_bind()
TYPE =
∀b:B
.not (eq B b Abst)
→∀c:C
.∀u:T
.sn3 c u
→∀vs:TList
.∀t:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O vs) t)
→sn3 c (THeads (Flat Appl) vs (THead (Bind b) u t))
BODY =
assume b: B
suppose H: not (eq B b Abst)
assume c: C
assume u: T
suppose H0: sn3 c u
assume vs: TList
we proceed by induction on vs to prove
∀t0:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O vs) t0)
→sn3 c (THeads (Flat Appl) vs (THead (Bind b) u t0))
case TNil : ⇒
the thesis becomes
∀t:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O TNil) t)
→sn3 c (THeads (Flat Appl) TNil (THead (Bind b) u t))
assume t: T
we must prove
(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O TNil) t)
→sn3 c (THeads (Flat Appl) TNil (THead (Bind b) u t))
or equivalently
sn3 (CHead c (Bind b) u) t
→sn3 c (THeads (Flat Appl) TNil (THead (Bind b) u t))
suppose H1: sn3 (CHead c (Bind b) u) t
by (sn3_bind . . . H0 . H1)
we proved sn3 c (THead (Bind b) u t)
that is equivalent to sn3 c (THeads (Flat Appl) TNil (THead (Bind b) u t))
we proved
sn3 (CHead c (Bind b) u) t
→sn3 c (THeads (Flat Appl) TNil (THead (Bind b) u t))
that is equivalent to
(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O TNil) t)
→sn3 c (THeads (Flat Appl) TNil (THead (Bind b) u t))
∀t:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O TNil) t)
→sn3 c (THeads (Flat Appl) TNil (THead (Bind b) u t))
case TCons ⇒
we need to prove
∀v:T
.∀vs0:TList
.∀t0:T
.sn3 (CHead c (Bind b) u) (THeads (Flat Appl) (lifts (S O) O vs0) t0)
→sn3 c (THeads (Flat Appl) vs0 (THead (Bind b) u t0))
→∀t0:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O (TCons v vs0)) t0)
→sn3 c (THeads (Flat Appl) (TCons v vs0) (THead (Bind b) u t0))
assume v: T
assume vs0: TList
we proceed by induction on vs0 to prove
∀t0:T
.sn3 (CHead c (Bind b) u) (THeads (Flat Appl) (lifts (S O) O vs0) t0)
→sn3 c (THeads (Flat Appl) vs0 (THead (Bind b) u t0))
→∀t0:T
.(sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O v
THeads (Flat Appl) (lifts (S O) O vs0) t0)
→(sn3
c
THead
Flat Appl
v
THeads (Flat Appl) vs0 (THead (Bind b) u t0))
case TNil : ⇒
the thesis becomes
∀t:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O TNil) t)
→sn3 c (THeads (Flat Appl) TNil (THead (Bind b) u t))
→∀t:T
.(sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O v
THeads (Flat Appl) (lifts (S O) O TNil) t)
→(sn3
c
THead
Flat Appl
v
THeads (Flat Appl) TNil (THead (Bind b) u t))
suppose :
∀t:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O TNil) t)
→sn3 c (THeads (Flat Appl) TNil (THead (Bind b) u t))
assume t: T
suppose H2:
sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O v
THeads (Flat Appl) (lifts (S O) O TNil) t
consider H2
we proved
sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O v
THeads (Flat Appl) (lifts (S O) O TNil) t
that is equivalent to
sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O v) t)
by (sn3_appl_bind . H . . H0 . . previous)
we proved sn3 c (THead (Flat Appl) v (THead (Bind b) u t))
that is equivalent to
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) TNil (THead (Bind b) u t)
∀t:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O TNil) t)
→sn3 c (THeads (Flat Appl) TNil (THead (Bind b) u t))
→∀t:T
.(sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O v
THeads (Flat Appl) (lifts (S O) O TNil) t)
→(sn3
c
THead
Flat Appl
v
THeads (Flat Appl) TNil (THead (Bind b) u t))
case TCons : t:T t0:TList ⇒
the thesis becomes
∀H2:∀t1:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)
→sn3 c (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1))
.∀t1:T
.∀H3:sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O v
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1
.sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)
() by induction hypothesis we know
∀t1:T
.sn3 (CHead c (Bind b) u) (THeads (Flat Appl) (lifts (S O) O t0) t1)
→sn3 c (THeads (Flat Appl) t0 (THead (Bind b) u t1))
→∀t1:T
.(sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O v
THeads (Flat Appl) (lifts (S O) O t0) t1)
→(sn3
c
THead
Flat Appl
v
THeads (Flat Appl) t0 (THead (Bind b) u t1))
suppose H2:
∀t1:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)
→sn3 c (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1))
assume t1: T
suppose H3:
sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O v
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1
(H_x)
by (sn3_gen_flat . . . . H3)
land
sn3 (CHead c (Bind b) u) (lift (S O) O v)
sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1
end of H_x
(H4) consider H_x
consider H4
we proved
land
sn3 (CHead c (Bind b) u) (lift (S O) O v)
sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1
that is equivalent to
land
sn3 (CHead c (Bind b) u) (lift (S O) O v)
sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O t
THeads (Flat Appl) (lifts (S O) O t0) t1
we proceed by induction on the previous result to prove
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)
case conj : H5:sn3 (CHead c (Bind b) u) (lift (S O) O v) H6:sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O t) (THeads (Flat Appl) (lifts (S O) O t0) t1)) ⇒
the thesis becomes
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)
(H_y)
by (sn3_gen_lift . . . . H5 .)
(drop (S O) O (CHead c (Bind b) u) c)→(sn3 c v)
end of H_y
(h1)
consider H6
we proved
sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O t
THeads (Flat Appl) (lifts (S O) O t0) t1
that is equivalent to
sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1
by (H2 . previous)
sn3 c (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1))
end of h1
(h2)
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) u) c
by (H_y previous)
sn3 c v
end of h2
(h3)
assume u2: T
suppose H7: pr3 c (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)) u2
suppose H8:
iso (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)) u2
→∀P:Prop.P
(H9)
by (pr3_iso_appls_bind . H . . . . . H7 H8)
pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1
u2
end of H9
(h1)
by (sn3_appl_bind . H . . H0 . . H3)
sn3
c
THead
Flat Appl
v
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1
end of h1
(h2)
by (pr3_refl . .)
we proved pr3 c v v
by (pr3_flat . . . previous . . H9 .)
pr3
c
THead
Flat Appl
v
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1
THead (Flat Appl) v u2
end of h2
by (sn3_pr3_trans . . h1 . h2)
we proved sn3 c (THead (Flat Appl) v u2)
∀u2:T
.pr3 c (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)) u2
→(iso (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)) u2
→∀P:Prop.P
→sn3 c (THead (Flat Appl) v u2))
end of h3
by (sn3_appl_appls . . . . h1 . h2 h3)
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)
we proved
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)
∀H2:∀t1:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)
→sn3 c (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1))
.∀t1:T
.∀H3:sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O v
THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1
.sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)
we proved
∀t0:T
.sn3 (CHead c (Bind b) u) (THeads (Flat Appl) (lifts (S O) O vs0) t0)
→sn3 c (THeads (Flat Appl) vs0 (THead (Bind b) u t0))
→∀t0:T
.(sn3
CHead c (Bind b) u
THead
Flat Appl
lift (S O) O v
THeads (Flat Appl) (lifts (S O) O vs0) t0)
→(sn3
c
THead
Flat Appl
v
THeads (Flat Appl) vs0 (THead (Bind b) u t0))
that is equivalent to
∀t0:T
.sn3 (CHead c (Bind b) u) (THeads (Flat Appl) (lifts (S O) O vs0) t0)
→sn3 c (THeads (Flat Appl) vs0 (THead (Bind b) u t0))
→∀t0:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O (TCons v vs0)) t0)
→sn3 c (THeads (Flat Appl) (TCons v vs0) (THead (Bind b) u t0))
∀v:T
.∀vs0:TList
.∀t0:T
.sn3 (CHead c (Bind b) u) (THeads (Flat Appl) (lifts (S O) O vs0) t0)
→sn3 c (THeads (Flat Appl) vs0 (THead (Bind b) u t0))
→∀t0:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O (TCons v vs0)) t0)
→sn3 c (THeads (Flat Appl) (TCons v vs0) (THead (Bind b) u t0))
we proved
∀t0:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O vs) t0)
→sn3 c (THeads (Flat Appl) vs (THead (Bind b) u t0))
we proved
∀b:B
.not (eq B b Abst)
→∀c:C
.∀u:T
.sn3 c u
→∀vs:TList
.∀t0:T
.(sn3
CHead c (Bind b) u
THeads (Flat Appl) (lifts (S O) O vs) t0)
→sn3 c (THeads (Flat Appl) vs (THead (Bind b) u t0))