Theorem: disconempty (Pdl/Discon.lean)

State before:
⊢ discon {∅} = ⊤
Tactic:
rfl
State after:
no goals