Step * of Lemma length-map

[f:Top]. ∀[T:Type]. ∀[L:T List].  (||map(f;L)|| ||L||)
BY
(InductionOnList THEN Reduce THEN EqCD THEN Trivial) }


Latex:


Latex:
\mforall{}[f:Top].  \mforall{}[T:Type].  \mforall{}[L:T  List].    (||map(f;L)||  \msim{}  ||L||)


By


Latex:
(InductionOnList  THEN  Reduce  0  THEN  EqCD  THEN  Trivial)




Home Index