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