Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. eq:T T . L1,L2:T List. x:T. disjoint(eq;(x::L1);L2) disjoint(eq;L1;L2)

Applied Tactic: UnivCD THENA Auto
Generated subgoals:

1. disjoint(eq;L1;L2)