intro W M w
a b : Program
p : ℕ
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p)) ∧ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p))
a b : Program
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p)) ∧ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p))