refine ⟨h2, ?_⟩
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
⊢ x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
⊢ ∀ m < 2, 0 < m → x ^ m ≠ 1