Theorem: ProgramUnionNotSelfContainingRight' (Pdl/DagSyntax.lean)

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

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