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