Level: Lib Thy Top:
Hypotheses:None
Conclusion:
T:
. Discrete{T} 
(eq1,eq2:{T
}. L,M:T List. eq1 = eq2 L(~eq1)M M(~eq2)L)
Applied Tactic: D 0 THENA Auto THEN
D 0 THENA Auto THEN
D 0 THENA Auto THEN
Equivalence (-1) THEN
D 0 THENA Auto THEN
Equivalence (-1) THEN
UnivCD THENA Auto
Generated subgoals:1. M(~eq2)L