---

Step * of Lemma map-append-empty2

∀[f,b:Top].  (map(f;b) @ [] ~ map(f;b))
BY
{ (SqReasoning
   THEN Try (Complete ((BLemma `append-nil-sqle` THEN Auto)))
   THEN (BLemma `sqle-append-nil-if-has-value3` THENA Auto)
   THEN BLemma `is-list-if-has-value-rec-map`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f,b:Top].    (map(f;b)  @  []  \msim{}  map(f;b))


By

---

Latex:
(SqReasoning
  THEN  Try  (Complete  ((BLemma  `append-nil-sqle`  THEN  Auto)))
  THEN  (BLemma  `sqle-append-nil-if-has-value3`  THENA  Auto)
  THEN  BLemma  `is-list-if-has-value-rec-map`
  THEN  Auto)

---

Home Index