Nuprl - Pf assert_rel

(2steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

a,b:rel(). rel_eq(a;b) a = b

By: UnivCD THEN Unfold `rel_eq` 0 THEN RW assert_pushdownC 0 THEN RWW "assert_eq_relname" 0 THEN RWW "assert_termlist_eq" 0 THEN Try ((HypSubst -1 0) THEN (Complete Auto))

Generated subgoal:

1 1. a: rel()
2. b: rel()
3. a.name = b.name
4. a.args = b.args
a = b

About:

(2steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc