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

At: eq lbl iff 2
1. l1: Label
2. l2: Label
3. l1 = l2

l1 = l2
By: Subst (l1 ~ l2) 0
Generated subgoal:

1 l2 = l2

About:
assertequalsqequal

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