Theorem: undag_inject (Pdl/DagSyntax.lean)

State before:
ps : List Program
α : Program
φ : Formula
⊢ undag (inject ps α φ) = ⌈⌈ps⌉⌉⌈∗α⌉φ
Tactic:
simp
State after:
no goals