Step
*
of Lemma
no_repeats_nil_uiff
∀[T:Top]. uiff(no_repeats(T;[]);True)
BY
{ (RepUR ``no_repeats`` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[T:Top].  uiff(no\_repeats(T;[]);True)
By
Latex:
(RepUR  ``no\_repeats``  0  THEN  Auto)
Home
Index