(6steps)
PrintForm
Definitions
Lemmas
mb
label
Sections
GenAutomata
Doc
At:
lbl
sq
1
1
1
2
1.
x:
Pattern
2.
ground_ptn(x)
3.
y:
Pattern
4.
ground_ptn(y)
5.
x = y
Label
6.
x,y:Pattern. x = y
(x ~ y)
7.
x ~ y
x ~ y
By:
Unfold `guard` 0
Generated subgoals:
None
About:
(6steps)
PrintForm
Definitions
Lemmas
mb
label
Sections
GenAutomata
Doc