all_goals try (simp; done)
case bot
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con [⊥]) ↔ evaluate M w (discon ∅)

case not
W : Type
M : KripkeModel W
w : W
φ✝ : Formula
⊢ evaluate M w (Con [φ✝, ~φ✝]) ↔ evaluate M w (discon ∅)

case neg
W : Type
M : KripkeModel W
w : W
φ✝ : Formula
⊢ evaluate M w (Con [~~φ✝]) ↔ evaluate M w (discon [[φ✝]])

case con
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [φ✝⋀ψ✝]) ↔ evaluate M w (discon [[φ✝, ψ✝]])

case nCo
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [~φ✝⋀ψ✝]) ↔ evaluate M w (discon [[~φ✝], [~ψ✝]])

case box
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldBox α✝ φ✝))

case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
case box
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldBox α✝ φ✝))

case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))