(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