constructor
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y ∧ y ∉ binders ↔ v = y
case mp
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y ∧ y ∉ binders → v = y

case mpr
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y → v = y ∧ y ∉ binders