---

Step * of Lemma hd-append-sq

∀[L1:Top List+]. ∀[L2:Top].  (hd(L1 @ L2) ~ hd(L1))
BY
{ ((UnivCD THENA Auto) THEN (D (-2) THENA Auto) THEN D (-3) THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L1:Top  List\msupplus{}].  \mforall{}[L2:Top].    (hd(L1  @  L2)  \msim{}  hd(L1))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (D  (-2)  THENA  Auto)  THEN  D  (-3)  THEN  All  Reduce  THEN  Auto)

---

Home Index