have := h ▸ selection x
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = pos x⁻¹
⊢ False
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = pos x⁻¹
this : xor (pos x⁻¹) (pos x⁻¹) = true
⊢ False