Theorem: ProgramStarNotSelfContain (Pdl/DagSyntax.lean)

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

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