exact nonOcc.left
case left.a
x : ℕ
ρ φ : Formula
F : List Formula
IH : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ vocabOfFormula φ ∧ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfFormula φ
no goals