Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

Discrete{Sequent}

Applied Tactic: InstLemma `discrete__Formula` []
Generated subgoals:

1. Discrete{Sequent}