Theorem: boxes_append (Pdl/Syntax.lean)

State before:
as bs : List Program
P : Formula
⊢ (⌈⌈as ++ bs⌉⌉P) = ⌈⌈as⌉⌉⌈⌈bs⌉⌉P
Tactic:
induction as
State after:
case nil
bs : List Program
P : Formula
⊢ (⌈⌈[] ++ bs⌉⌉P) = ⌈⌈[]⌉⌉⌈⌈bs⌉⌉P

case cons
bs : List Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P
⊢ (⌈⌈head✝ :: tail✝ ++ bs⌉⌉P) = ⌈⌈head✝ :: tail✝⌉⌉⌈⌈bs⌉⌉P

State before:
case nil
bs : List Program
P : Formula
⊢ (⌈⌈[] ++ bs⌉⌉P) = ⌈⌈[]⌉⌉⌈⌈bs⌉⌉P
Tactic:
simp
State after:
no goals

State before:
case cons
bs : List Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P
⊢ (⌈⌈head✝ :: tail✝ ++ bs⌉⌉P) = ⌈⌈head✝ :: tail✝⌉⌉⌈⌈bs⌉⌉P
Tactic:
simp at *
State after:
case cons
bs : List Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P
⊢ (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P

State before:
case cons
bs : List Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P
⊢ (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P
Tactic:
assumption
State after:
no goals