rw [localDiamondTruth α φ W M w, disEval, disconEval]
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (~⌈α⌉φ) ↔ evaluate M w (discon (List.map (fun Fδ => Yset Fδ φ) (H α)))
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ f ∈ List.map (fun Fδ => Con (Yset Fδ φ)) (H α), evaluate M w f) ↔
    ∃ Y ∈ List.map (fun Fδ => Yset Fδ φ) (H α), ∀ f ∈ Y, evaluate M w f