. intro iv₁ iv₂
  simp only [Subtype.mk.injEq, Prod.mk.injEq, and_imp]
  intro hfst hsnd
  cases iv₁; cases iv₂; cases hfst; cases hsnd; rfl
case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂
no goals