simp only [isFreeIn] at h1
case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (def_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (def_ a✝¹ a✝) = fastReplaceFree σ' (def_ a✝¹ a✝)
case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ fastReplaceFree σ (def_ a✝¹ a✝) = fastReplaceFree σ' (def_ a✝¹ a✝)