---

Step * of Lemma null-map

∀[f,L:Top].  (null(map(f;L)) ~ null(L))
BY
{ ((((UnivCD THENA Auto) THEN Unfolds ``map null`` 0) THEN RecUnfold `list_ind` 0)
   THEN SqReasoning
   THEN Try (RepeatFor 2 ((HVimplies2 0 [2] THEN (RWO "-1" 0 THENA Auto))))
   THEN Try (RepeatFor 2 ((HVimplies2 0 [1] THEN (RWO "-1" 0 THENA Auto))))) }

---

Latex:

---

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


By

---

Latex:
((((UnivCD  THENA  Auto)  THEN  Unfolds  ``map  null``  0)  THEN  RecUnfold  `list\_ind`  0)
  THEN  SqReasoning
  THEN  Try  (RepeatFor  2  ((HVimplies2  0  [2]  THEN  (RWO  "-1"  0  THENA  Auto))))
  THEN  Try  (RepeatFor  2  ((HVimplies2  0  [1]  THEN  (RWO  "-1"  0  THENA  Auto)))))

---

Home Index