Nuprl - Pf assert term eq 1 2

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

1. a: Tree(ts())
2. u: Tree(ts())Type{i'}
3. w: a:{v:Tree(ts())| u(v) }b:Tree(ts()). term_eq(a;b) a = b
4. x: ts()
5. b: Tree(ts())
6. u1: Tree(ts())Type{i'}
7. w1: b:{v:Tree(ts())| u1(v) }term_eq(tree_leaf(x);b) tree_leaf(x) = b Tree(ts())
8. x1: ts()
9. tree_leaf(x) = tree_leaf(x1) Tree(ts())

x = x1

By: ApFunToHypEquands `z' Case(z) Case tree_leaf(u) = > u Default = > x ts() -1 THEN Reduce -1

Generated subgoal:

1 10. z: Tree(ts())
Case(z) Case tree_leaf(u) = > u Default = > x = Case(z) Case tree_leaf(u) = > u Default = > x ts()

About:

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