Theorem: A2 (Pdl/Examples.lean)

State before:
a : Program
⊢ tautology (⌈a⌉⊤)
Tactic:
unfold tautology
State after:
a : Program
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (⌈a⌉⊤)

State before:
a : Program
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (⌈a⌉⊤)
Tactic:
simp
State after:
no goals