Theorem: ProgramSequenceNotSelfContaining (Pdl/DagSyntax.lean)

State before:
⊢ ∀ (p q : Program), ¬p = (p;'q)
Tactic:
intro p q hyp
State after:
p q : Program
hyp : p = (p;'q)
⊢ False

State before:
p q : Program
hyp : p = (p;'q)
⊢ False
Tactic:
cases hyp
State after:
no goals