contrapose! rhs
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
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 : ¬False
⊢ (∀ (v : W), relate M a w v → evaluate M v X) ∧ ∀ (x : W), relate M b w x → evaluate M x X