Step * of Lemma bag_qinc

A:Type. ((A List) ⊆bag(A))
BY
(Unfold `bag` THEN Auto) }


Latex:


Latex:
\mforall{}A:Type.  ((A  List)  \msubseteq{}r  bag(A))


By


Latex:
(Unfold  `bag`  0  THEN  Auto)




Home Index