Theorem: mytaut2 (Pdl/Examples.lean)

State before:
p : ℕ
⊢ tautology (~(~~·p)⋀(~·p))
Tactic:
unfold tautology evaluate
State after:
p : ℕ
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), ¬evaluate M w ((~~·p)⋀(~·p))

State before:
p : ℕ
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), ¬evaluate M w ((~~·p)⋀(~·p))
Tactic:
intro W M w
State after:
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ ¬evaluate M w ((~~·p)⋀(~·p))

State before:
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ ¬evaluate M w ((~~·p)⋀(~·p))
Tactic:
simp
State after:
no goals