apply repl_in_F_non_occ_eq
case right
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ repl_in_F x ρ φ2 = φ2
case right.a
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ x ∉ voc φ2