Nuprl - Pf singelton append equals lemma 1

(9steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

1. T: Type
2. a: T
3. R: T List
4. S: T List
5. b: T
6. [a] = (R @ (b.S))

a = b

By: ListInd 3 THEN AbReduce 0 THEN Thin 3

Generated subgoals:

1 3. S: T List
4. b: T
5. [a] = b.S
a = b

2 3. S: T List
4. b: T
5. u: T
6. v: T List
7. [a] = (v @ (b.S)) a = b
8. [a] = u.(v @ (b.S))
a = b

About:

(9steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

1	3. `S:` `T List` 4. `b:` `T` 5. `[a] = b.S` `a = b`
2	3. `S:` `T List` 4. `b:` `T` 5. `u:` `T` 6. `v:` `T List` 7. `[a] = (v @ (b.S)) a = b` 8. `[a] = u.(v @ (b.S))` `a = b`