Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
Discrete{Atom}
Applied Tactic:
Unfold `discrete` 0 THEN UnivCD THENA Auto THEN ProveDecidable THEN Auto
Generated subgoals:
None
Discrete{Atom}