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

At: append associative 1 2 1
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: MemberEqCD
Generated subgoals:

None

About:
listconsuniverseequal

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