case inr hyp =>
  have IHβ := existsDiamondH hyp
  aesop
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
no goals