simp only [Rec.fastReplaceFree]
case def_
F F' : Formula
v u : VarName
X✝ : DefName
xs✝ : List VarName
v✝ t✝ : VarName
⊢ Rec.fastReplaceFree v✝ t✝ (def_ X✝ xs✝) = def_ X✝ (List.map (fun x => if v✝ = x then t✝ else x) xs✝)
no goals