case _ x =>
  constructor
  case mp =>
    tauto
  case mpr =>
    intro a1
    subst a1
    tauto
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
⊢ v = x ∧ x ∉ binders ↔ v = x
no goals