Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
eq:{T
}.
L,M:T List. L(~eq)M
M(~eq)L
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
. L(~eq)M
M(~eq)L
T:
. eq:{T
}. L,M:T List. L(~eq)M 
M(~eq)L M(~eq)L