rw [repl_in_dis, listEq_to_disEq]
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ repl_in_F x ρ (dis (List.map (fun Fδ => if p Fδ then Formula.bottom else f Fδ) L)) =
    dis (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 ρ) (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