Theorem: ProgramTestNotSelfContain (Pdl/DagSyntax.lean)

State before:
ψ : DagFormula
φ : Formula
⊢ ¬ψ = ⌈?'φ⌉ψ
Tactic:
intro hyp
State after:
ψ : DagFormula
φ : Formula
hyp : ψ = ⌈?'φ⌉ψ
⊢ False

State before:
ψ : DagFormula
φ : Formula
hyp : ψ = ⌈?'φ⌉ψ
⊢ False
Tactic:
cases hyp
State after:
no goals