Theorem: consingle (Pdl/Discon.lean)

State before:
f : Formula
⊢ Con [f] = f
Tactic:
rfl
State after:
no goals