---

Step * 1 of Lemma sqequal-append-cbva-weak2


∀[b,F:Top].  (let x ⟵ [] @ b in F[x] ~ let u ⟵ [] in let v ⟵ b in let x ⟵ u @ v in F[x])
BY
{ (Reduce 0
   THEN (UnivCD THENA Auto)
   THEN SqEqualBase
   THEN UseCbvaSq
   THEN (RWO "evalall-sqequal" 0 THEN Auto)
   THEN CallByValueReduce 0
   THEN Auto) }

---

Latex:

---

Latex:

\mforall{}[b,F:Top].    (let  x  \mleftarrow{}{}  []  @  b  in  F[x]  \msim{}  let  u  \mleftarrow{}{}  []  in  let  v  \mleftarrow{}{}  b  in  let  x  \mleftarrow{}{}  u  @  v  in  F[x])


By

---

Latex:
(Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  SqEqualBase
  THEN  UseCbvaSq
  THEN  (RWO  "evalall-sqequal"  0  THEN  Auto)
  THEN  CallByValueReduce  0
  THEN  Auto)

---

Home Index