Theorem: undag_boxes (Pdl/DagSyntax.lean)

State before:
ps : List Program
df : DagFormula
⊢ undagDagFormula (⌈⌈ps⌉⌉df) = ⌈⌈ps⌉⌉undag df
Tactic:
cases ps
State after:
case nil
df : DagFormula
⊢ undagDagFormula (⌈⌈[]⌉⌉df) = ⌈⌈[]⌉⌉undag df

case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈head✝ :: tail✝⌉⌉df) = ⌈⌈head✝ :: tail✝⌉⌉undag df

State before:
case nil
df : DagFormula
⊢ undagDagFormula (⌈⌈[]⌉⌉df) = ⌈⌈[]⌉⌉undag df

case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈head✝ :: tail✝⌉⌉df) = ⌈⌈head✝ :: tail✝⌉⌉undag df
Tactic:
simp
State after:
case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈head✝ :: tail✝⌉⌉df) = ⌈⌈head✝ :: tail✝⌉⌉undag df

State before:
case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈head✝ :: tail✝⌉⌉df) = ⌈⌈head✝ :: tail✝⌉⌉undag df
Tactic:
simp
State after:
case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈tail✝⌉⌉df) = ⌈⌈tail✝⌉⌉undagDagFormula df

State before:
case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈tail✝⌉⌉df) = ⌈⌈tail✝⌉⌉undagDagFormula df
Tactic:
apply undag_boxes
State after:
no goals