case union α β =>
  simp [H, relateSeq] at *
  cases v_γ_w
  case inl hyp =>
    have IHα := existsDiamondH hyp
    aesop
  case inr hyp =>
    have IHβ := existsDiamondH hyp
    aesop
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M (α⋓β) v w
⊢ ∃ Fδ ∈ H (α⋓β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
no goals