Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

Dec(True)

Applied Tactic: Unfold `decidable` 0
Generated subgoals:

1. True True