simp only [List.map_cons, List.cons.injEq]
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ List.map (repl_in_F x ρ) (φ :: F) = φ :: F
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ repl_in_F x ρ φ = φ ∧ List.map (repl_in_F x ρ) F = F