constructor
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ var v = var v' ↔ v = v'
case mp
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ var v = var v' → v = v'

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ v = v' → var v = var v'