Theorem: loadBoxes_last (Pdl/Syntax.lean)

State before:
a : Program
as : List Program
c : Program
P : LoadFormula
⊢ (~'⌊a⌋⌊⌊as ++ [c]⌋⌋P) = ~'⌊a⌋⌊⌊as⌋⌋⌊c⌋P
Tactic:
induction as
State after:
case nil
a c : Program
P : LoadFormula
⊢ (~'⌊a⌋⌊⌊[] ++ [c]⌋⌋P) = ~'⌊a⌋⌊⌊[]⌋⌋⌊c⌋P

case cons
a c : Program
P : LoadFormula
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 : LoadFormula
⊢ (~'⌊a⌋⌊⌊[] ++ [c]⌋⌋P) = ~'⌊a⌋⌊⌊[]⌋⌋⌊c⌋P
Tactic:
simp
State after:
no goals

State before:
case cons
a c : Program
P : LoadFormula
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 : LoadFormula
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 : LoadFormula
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