Step
*
of Lemma
map-axiom
∀[f:Top]. (map(f;Ax) ~ Ax)
BY
{ (Fold `it` 0 THEN Fold `nil` 0 THEN Reduce 0 THEN Auto) }
Latex:
Latex:
\mforall{}[f:Top].  (map(f;Ax)  \msim{}  Ax)
By
Latex:
(Fold  `it`  0  THEN  Fold  `nil`  0  THEN  Reduce  0  THEN  Auto)
Home
Index