rintro rfl
case inr.left
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
⊢ ¬a = x
case inr.left
X : Type u_1
inst✝ : ProperInvolutiveInv X
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
h : a ∉ ↑(maxInvFreeSet X)
⊢ False