have IHβ := localDiamondTruth β ψ W M w
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : evaluate M w (~⌈α⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H α)))
⊢ evaluate M w (~⌈α⋓β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α⋓β))))
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : evaluate M w (~⌈α⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H α)))
IHβ : evaluate M w (~⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
⊢ evaluate M w (~⌈α⋓β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α⋓β))))