Nuprl - Pf eq_lbl_iff 2 1

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

At: eq lbl iff 2 1

1. l1: Label
2. l2: Label
3. l1 = l2

l2 = l2

By: EqLblReflexive 0 THEN Trivial

Generated subgoals:

None

About:

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