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

At: lbl pair wf2 1 2
1. x: Label
2. y: Label

ground_ptn(lbl_pr( < x, y > ))
By:
RecUnfold `ground_ptn` 0
THEN
Reduce 0
Generated subgoal:

1 ground_ptn(x)ground_ptn(y)

About:
assert

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