case eq_ x y =>
  congr!
  case _ | _ =>
    constructor
    case mp =>
      tauto
    case mpr =>
      intro a1
      subst a1
      tauto
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ eq_ (if v = x ∧ x ∉ binders then t else x) (if v = y ∧ y ∉ binders then t else y) =
    eq_ (if v = x then t else x) (if v = y then t else y)
no goals