simp [evaluate, H, Yset, disEval] at *
ψ : 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 (α⋓β))))
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ (∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ) ↔
    ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f