---

Step * of Lemma iterate-hdf-append

∀[L1:Top List]. ∀[F,L2:Top].  (F*(L1 @ L2) ~ F*(L1)*(L2))
BY
{ (InductionOnList THEN Reduce 0 THEN (UnivCD THENA Auto) THEN RWW "-3" 0 THEN Auto) }

---

Latex:


\mforall{}[L1:Top  List].  \mforall{}[F,L2:Top].    (F*(L1  @  L2)  \msim{}  F*(L1)*(L2))


By

(InductionOnList  THEN  Reduce  0  THEN  (UnivCD  THENA  Auto)  THEN  RWW  "-3"  0  THEN  Auto)

---

Home Index