cases v_γ_w
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M α v w ∨ relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
case inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
h✝ : relate M α v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w

case inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
h✝ : relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w