Nuprl - Pf singelton append equals lemma 1 1

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

a = b

By: ListInd 3 THEN AbReduce 0 THEN Thin 3

Generated subgoals:

1 3. b: T
4. [a] = [b]
a = b

2 3. b: T
4. u: T
5. v: T List
6. [a] = b.v a = b
7. [a] = [b; u/ v]
a = b

About:

1	3. `b:` `T` 4. `[a] = [b]` `a = b`
2	3. `b:` `T` 4. `u:` `T` 5. `v:` `T List` 6. `[a] = b.v a = b` 7. `[a] = [b; u/ v]` `a = b`