Nuprl - Proof: sublist append iff 1 1

(16steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

1. T: Type
2. C: T List
3. u: T
4. v: T List
5. A,B:T List. v A @ B (A',B':T List. v = (A' @ B') & A' A & B' B)
6. A: T List
7. u1: T
8. v1: T List
9. B:T List. [u / v] v1 @ B (A',B':T List. [u / v] = (A' @ B') & A' v1 & B' B)
10. B: T List
11. u = u1 & v v1 @ B [u / v] v1 @ B

A',B':T List. [u / v] = (A' @ B') & A' [u1 / v1] & B' B

By: Analyze -1

Generated subgoals:

1 11. u = u1
12. v v1 @ B
A',B':T List. [u / v] = (A' @ B') & A' [u1 / v1] & B' B 3 steps

2 11. [u / v] v1 @ B
A',B':T List. [u / v] = (A' @ B') & A' [u1 / v1] & B' B 2 steps

About:

(16steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

1	11. `u = u1` 12. `v v1 @ B` `A',B':T List. [u / v] = (A' @ B') & A' [u1 / v1] & B' B`	3 steps

2	11. `[u / v] v1 @ B` `A',B':T List. [u / v] = (A' @ B') & A' [u1 / v1] & B' B`	2 steps