simp at *
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
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