Theorem: boxTop (Bml/Examples.lean)

State before:
⊢ Tautology (□⊤)
Tactic:
unfold Tautology Evaluate
State after:
⊢ ∀ (W : Type) (M : KripkeModel W) (w v : W), M.Rel w v → Evaluate (M, v) ⊤

State before:
⊢ ∀ (W : Type) (M : KripkeModel W) (w v : W), M.Rel w v → Evaluate (M, v) ⊤
Tactic:
tauto
State after:
no goals