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

At: append associative 1 2
1. T: Type
2. L1: T List
3. L2: T List
4. L3: T List
5. u: T
6. v: T List
7. (v @ L2 @ L3) = ((v @ L2) @ L3)

((u.v) @ L2 @ L3) = (((u.v) @ L2) @ L3)
By: Reduce 0
Generated subgoal:

1 u.(v @ L2 @ L3) = u.((v @ L2) @ L3)

About:
listconsuniverseequal

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