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

At: singelton append equals lemma

T:Type, a:T, R,S:T List, b:T. [a] = (R @ (b.S)) a = b
By: UnivCD
Generated subgoal:

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

About:
listconsconsniluniverseequalimpliesall

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