intro d d_in
case right
x : ℕ
ρ φ : Formula
F : List Formula
nonOcc : x ∉ vocabOfFormula φ ∧ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
⊢ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
case right
x : ℕ
ρ φ : Formula
F : List Formula
nonOcc : x ∉ vocabOfFormula φ ∧ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
d : Formula
d_in : d ∈ F
⊢ x ∉ vocabOfFormula d