Nuprl - Pf assert_lbls

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

1. x: Label
2. ls: Label List
3. u: Label
4. v: Label List
5. x v (x v)

x [u / v] (x [u / v])

By: RWW "cons_member" 0 THEN Unfold `lbls_member` 0 THEN Reduce 0 THEN Fold `lbls_member` 0 THEN RW assert_pushdownC 0 THEN Reduce 0 THEN Analyze -1 THEN ThinTrivial THEN Try (Complete (Sel 2 (Analyze 0))) THEN Sel 1 (Analyze 0)

Generated subgoals:

1 5. x v (x v)
6. x v (x v)
7. x = u
x = u

2 5. x v (x v)
6. x v (x v)
7. x = u
x = u

About:

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

1	5. `x v (x v)` 6. `x v (x v)` 7. `x = u` `x = u`
2	5. `x v (x v)` 6. `x v (x v)` 7. `x = u` `x = u`