---

Step * of Lemma callbyvalueall-single-bag-combine4

No Annotations
∀[F,a:Top].  (let x ⟵ [a] in F[x] ~ let x ⟵ a in F[[x]])
BY
{ ((UnivCD THENA Auto) THEN RW BasicSymbolicComputeC' 0 THEN Auto THEN Computation) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[F,a:Top].    (let  x  \mleftarrow{}{}  [a]  in  F[x]  \msim{}  let  x  \mleftarrow{}{}  a  in  F[[x]])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RW  BasicSymbolicComputeC'  0  THEN  Auto  THEN  Computation)

---

Home Index