Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
eq:{T
}.
L1,L2:T List. L1(~eq)L2
Applied Tactic:
Unfold `list_iso` 0 THEN Auto
Generated subgoals:
None
T:
. eq:{T
}. L1,L2:T List. L1(~eq)L2 