---

Step * of Lemma sqequal-append-cbva-weak3

∀[a:Top List]. ∀[b,F:Top].  (let u ⟵ a in let v ⟵ b in let x ⟵ u @ v in F[x] ~ let x ⟵ a @ b in F[x])
BY
{ ((UnivCD THENA Auto) THEN RWO "sqequal-append-cbva-weak2<" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "sqequal-append-cbva-weak2<"  0  THEN  Auto)

---

Home Index