Step
*
1
1
1
of Lemma
empty_bag_append_lemma
1. b : Top@i
⊢ b ~ b
BY
{ Try SqEqCD }
Latex:
Latex:
1.  b  :  Top@i
\mvdash{}  b  \msim{}  b
By
Latex:
Try  SqEqCD
Home
Index