rw [disEval]
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ f ∈ List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α), evaluate M w f) ↔
    evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ f ∈ List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α), evaluate M w f) ↔
    ∃ f ∈ List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β)), evaluate M w f