---

Step * of Lemma simple-cbva-seq-spread0

∀[F,G,H,L:Top].  (let x,y = simple-cbva-seq(L;<F, G>;0) in H[x;y] ~ simple-cbva-seq(L;H[F;G];0))
BY
{ (RepUR ``simple-cbva-seq cbva-seq`` 0 THEN RecUnfold `callbyvalueall-seq` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[F,G,H,L:Top].    (let  x,y  =  simple-cbva-seq(L;<F,  G>0)  in  H[x;y]  \msim{}  simple-cbva-seq(L;H[F;G];0))


By

---

Latex:
(RepUR  ``simple-cbva-seq  cbva-seq``  0  THEN  RecUnfold  `callbyvalueall-seq`  0  THEN  AutoSplit)

---

Home Index