Theorem: ProgramBoxStarNotSelfContain (Pdl/DagSyntax.lean)

State before:
α : Program
ψ : DagFormula
⊢ ¬(⌈∗α⌉ψ) = ψ
Tactic:
intro hyp
State after:
α : Program
ψ : DagFormula
hyp : (⌈∗α⌉ψ) = ψ
⊢ False

State before:
α : Program
ψ : DagFormula
hyp : (⌈∗α⌉ψ) = ψ
⊢ False
Tactic:
cases hyp
State after:
no goals