Step
*
of Lemma
empty_bag_append_lemma
∀b:Top. ({} + b ~ b)
BY
{ (UnivCD THENA Auto) }
1
1. b : Top@i
⊢ {} + b ~ b
Latex:
Latex:
\mforall{}b:Top. (\{\} + b \msim{} b)
By
Latex:
(UnivCD THENA Auto)
Home
Index