Step
*
of Lemma
length-map
∀[f:Top]. ∀[T:Type]. ∀[L:T List].  (||map(f;L)|| ~ ||L||)
BY
{ (InductionOnList THEN Reduce 0 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