Nuprl - Pf assert_eq_label 1 1

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

At: assert eq label 1 1

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

l1 = l2

By: Subst (l1 ~ l2) 0

Generated subgoals:

1 l1 ~ l2

2 l2 = l2

About:

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