Nuprl - Pf singelton append equals lemma 1 2

1. T: Type
2. a: T
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

By: MoveToConcl -1 THEN TryOnAllHyps Thin THEN ListInd -1 THEN AbReduce 0

Generated subgoals:

1 7. [a] = [u; b/ S]
a = b

2 7. u1: T
8. v1: T List
9. [a] = u.(v1 @ (b.S)) a = b
10. [a] = [u; u1/ v1 @ (b.S)]
a = b

About:

1	7. `[a] = [u; b/ S]` `a = b`
2	7. `u1:` `T` 8. `v1:` `T List` 9. `[a] = u.(v1 @ (b.S)) a = b` 10. `[a] = [u; u1/ v1 @ (b.S)]` `a = b`