Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
eq:T
T
.
L1,L2:T List. Dec(disjoint(eq;L1;L2))
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
. Dec(disjoint(eq;L1;L2))
T:
. eq:T 
T 
. L1,L2:T List. Dec(disjoint(eq;L1;L2))