simp
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(φ⋀⌈∗a⌉~φ⋀(~⌈a⌉φ))⋀(~⌈∗a⌉φ))
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w φ →
    (∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ) →
      ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ