apply repl_in_F_non_occ_eq
case right
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_F x ρ φ0 = φ0
case right.a
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ x ∉ voc φ0