case atom_prop c =>
  simp only [repl_in_F, beq_iff_eq, ite_eq_right_iff]
  intro c_is_x; simp [voc,vocabOfFormula] at *; tauto
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
⊢ repl_in_F x ρ (·c) = ·c
no goals