Nuprl - Pf assert_eq_label 1 1 1

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

At: assert eq label 1 1 1

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

l1 ~ l2

By: Analyze 1 THEN Analyze 3

Generated subgoals:

None

About:

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