Nuprl - Pf assert termlist eq 2 1 1

(13steps) PrintForm Definitions Lemmas mb automata 2 Sections GenAutomata Doc

1. a: Term List
2. u: Term
3. v: Term List
4. b:Term List. termlist_eq(v;b) v = b
5. b: Term List
6. u1: Term
7. v1: Term List
8. termlist_eq([u / v];v1) [u / v] = v1
9. termlist_eq([u / v];v1) ([u / v] = v1)
10. [u / v] = [u1 / v1]

u = u1

By: Assert ([u / v] = [u1 / v1])

Generated subgoals:

1 [u / v] = [u1 / v1] Term List

2 11. [u / v] = [u1 / v1] Term List
u = u1

About:

(13steps) PrintForm Definitions Lemmas mb automata 2 Sections GenAutomata Doc

1	`[u / v] = [u1 / v1] Term List`
2	11. `[u / v] = [u1 / v1] Term List` `u = u1`