clear IH
case right
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc F
case right
x : ℕ
ρ φ : Formula
F : List Formula
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc F