---

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:


\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

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

---

Home Index