case pred_const_ X xs | pred_var_ X xs | eq_ x y | def_ X xs =>
  apply Finset.ext
  intro a
  simp
c : Char
X : DefName
xs : List VarName
σ : VarName → VarName
⊢ (List.map σ xs).toFinset = Finset.image σ xs.toFinset
no goals