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

At: append commutes under sublist 1
1. T: Type
2. Discrete{T}
3. eq: {T}
4. L: T List
5. M: T List

(L @ M)(eq)(M @ L)
By: UnfoldTopAb 0
Generated subgoal:

1 x(L @ M).x(eq) (M @ L)

About:
listassertuniverse

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