Step * of Lemma single-bag-append-nil

[a:Top]. ([a] [] [a])
BY
(Auto THEN RepUR ``bag-append`` THEN Auto) }


Latex:


Latex:
\mforall{}[a:Top].  ([a]  +  []  \msim{}  [a])


By


Latex:
(Auto  THEN  RepUR  ``bag-append``  0  THEN  Auto)




Home Index