Nuprl - Pf singelton append equals lemma 1 1 1

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

a = b

By: ApFunToHypEquands `L' (Case of L; nil a ; h.t h) T -1 THEN Reduce -1

Generated subgoal:

1 5. a = b
a = b

About: