simp only [List.mem_singleton, forall_eq, discon, unfoldDiamond]
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∀ f ∈ [~⌈α⌉φ], evaluate M w f) ↔ evaluate M w (discon (unfoldDiamond α φ))
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (~⌈α⌉φ) ↔ evaluate M w (discon (List.map (fun Fδ => Yset Fδ φ) (H α)))