Nuprl - Pf assert_lbls_member 1

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

At: assert lbls member 1

1. x: Label
2. ls: Label List

x nil (x nil)

By: Unfolds [`l_member`;`lbls_member`] 0 THEN Reduce 0 THEN ExRepD

Generated subgoals:

None

About:

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