constructor
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ (v = x → x ∉ binders → t = x) ∧ (v = y → y ∉ binders → t = y)
case left
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v = x → x ∉ binders → t = x

case right
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v = y → y ∉ binders → t = y