Step * of Lemma nil_iseg

[T:Type]. ∀l:T List. [] ≤ l
BY
(Unfold `iseg` THEN Obvious) }


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}l:T  List.  []  \mleq{}  l


By


Latex:
(Unfold  `iseg`  0  THEN  Obvious)




Home Index