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

At: append associative

T:Type, L1,L2,L3:T List. (L1 @ L2 @ L3) = ((L1 @ L2) @ L3)
By: UnivCD
Generated subgoal:

11. T: Type
2. L1: T List
3. L2: T List
4. L3: T List
(L1 @ L2 @ L3) = ((L1 @ L2) @ L3)

About:
listuniverseequalall

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