Theorem: boxes_last (Pdl/Syntax.lean)

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

case cons
a c : Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (~⌈a⌉⌈⌈tail✝ ++ [c]⌉⌉P) = (~⌈a⌉⌈⌈tail✝⌉⌉⌈c⌉P)
⊢ (~⌈a⌉⌈⌈head✝ :: tail✝ ++ [c]⌉⌉P) = (~⌈a⌉⌈⌈head✝ :: tail✝⌉⌉⌈c⌉P)

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

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

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