(5steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

At: equal appends 1
1. T: Type
2. a: T List
c,b,d:T List. b = (c @ d) (e:T List. nil = (c @ e) & d = (e @ b) c = e & b = (e @ d))
By: Obvious
Generated subgoals:

None

About:
listniluniverseequalimpliesandorallexists

(5steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc