(5steps) PrintForm Definitions Lemmas mb label Sections GenAutomata Doc

At: assert lbls member 2 2
1. x: Label
2. ls: Label List
3. u: Label
4. v: Label List
5. x v (x v)
6. x v (x v)
7. x = u

x = u
By:
HypSubst -1 0
THEN
EqLblReflexive 0
Generated subgoals:

None

About:
listassertequalimplies

(5steps) PrintForm Definitions Lemmas mb label Sections GenAutomata Doc