Nuprl - Proof: append is singleton

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

T:Type, a,b:T List, x:T. [x] = (a @ b) a = nil & b = [x] b = nil & a = [x]

By: InductionOnList THEN Reduce 0

Generated subgoals:

1 1. T: Type
2. a: T List
b:T List, x:T. [x] = b nil = nil T List & b = [x] b = nil & nil = [x] 1 step

2 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] 3 steps

About:

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

1	1. `T:` `Type` 2. `a:` `T List` `b:T List, x:T. [x] = b nil = nil T List & b = [x] b = nil & nil = [x]`	1 step

2	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]`	3 steps