Theorem: ProgramUnionNotSelfContainingLeft' (Pdl/DagSyntax.lean)

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

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