simp only [Subtype.mk.injEq, Prod.mk.injEq, and_imp]
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
⊢ { val := (iv₁.fst, iv₁.snd),
        property :=
          (_ :
            ↑(iv₁.fst, iv₁.snd).fst < ↑(iv₁.fst, iv₁.snd).snd ∧
              ↑x[↑(iv₁.fst, iv₁.snd).fst] > ↑x[↑(iv₁.fst, iv₁.snd).snd]) } =
      { val := (iv₂.fst, iv₂.snd),
        property :=
          (_ :
            ↑(iv₂.fst, iv₂.snd).fst < ↑(iv₂.fst, iv₂.snd).snd ∧
              ↑x[↑(iv₂.fst, iv₂.snd).fst] > ↑x[↑(iv₂.fst, iv₂.snd).snd]) } →
    iv₁ = iv₂
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
⊢ iv₁.fst = iv₂.fst → iv₁.snd = iv₂.snd → iv₁ = iv₂