simp only [List.map_map]
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ List.map (repl_in_F x ρ) (List.map (fun Fδ => if p Fδ then Formula.bottom else f Fδ) L) =
    List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ List.map (repl_in_F x ρ ∘ fun Fδ => if p Fδ then Formula.bottom else f Fδ) L =
    List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L