cases' hyp with lhs rhs
case left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
hyp :
  (∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X) ∧
    ((∀ (v : W), relate M a w v → evaluate M v X) → ∃ x, relate M b w x ∧ ¬evaluate M x X)
⊢ False
case left.intro
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : (∀ (v : W), relate M a w v → evaluate M v X) → ∃ x, relate M b w x ∧ ¬evaluate M x X
⊢ False