Theorem: LO.StandardModalLogicalConnective.duality' (Logic/Modal/LogicSymbol.lean)

State before:
F : Type u_1
inst✝ : StandardModalLogicalConnective F
p : F
⊢ ◇p = ~(□~p)
Tactic:
apply duality
State after:
no goals