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

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

(M @ L)(eq)(L @ M)
By: BackThru Thm* Discrete{T} (eq:{T}, L,M:T List. (L @ M)(eq)(M @ L))
Generated subgoals:

None

About:
listuniverse

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