Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. Discrete{T} (eq:{T}. L,M:T List. (L @ M)(~eq)(M @ L))

Applied Tactic: Unfold `list_iso` 0 THEN UnivCD THENA Auto THEN D 0
Generated subgoals:

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

2. (M @ L)(eq)(L @ M)