unfold tautology evaluate
a : Program
X : Formula
⊢ tautology ((~(⌈∗a⌉X)⋀(~X⋀⌈a⌉⌈∗a⌉X))⋀(~(⌈∗a⌉X)⋀(~⌈∗a⌉X)))
a : Program
X : Formula
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (~(⌈∗a⌉X)⋀(~X⋀⌈a⌉⌈∗a⌉X)) ∧ evaluate M w (~(⌈∗a⌉X)⋀(~⌈∗a⌉X))