Theorem: loadBoxes_append (Pdl/Syntax.lean)

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

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

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