Nuprl - Proof: append is singleton 2

(5steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

1. T: Type
2. a: T List
3. u: T
4. v: T List
5. b:T List, x:T. [x] = (v @ b) v = nil & b = [x] b = nil & v = [x]

b:T List, x:T. [x] = [u / (v @ b)] [u / v] = nil & b = [x] b = nil & [u / v] = [x]

By: Auto THEN SplitCons -1 THEN OrRight

Generated subgoals:

1 6. b: T List
7. x: T
8. x = u
9. nil = (v @ b)
b = nil 1 step

2 6. b: T List
7. x: T
8. x = u
9. nil = (v @ b)
[u / v] = [x] 1 step

About:

(5steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

1	6. `b:` `T List` 7. `x:` `T` 8. `x = u` 9. `nil = (v @ b)` `b = nil`	1 step

2	6. `b:` `T List` 7. `x:` `T` 8. `x = u` 9. `nil = (v @ b)` `[u / v] = [x]`	1 step