Theorem: ProgramUnionNotSelfContainingRight (Pdl/DagSyntax.lean)

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

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