apply repl_in_P_non_occ_eq
case left
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_P x ρ α = α
case left.a
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ x ∉ voc α