Step * of Lemma length-singleton

[x:Top]. (||[x]|| 1)
BY
(Reduce THEN Auto) }


Latex:


Latex:
\mforall{}[x:Top].  (||[x]||  \msim{}  1)


By


Latex:
(Reduce  0  THEN  Auto)




Home Index