intro iv₁ iv₂
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₂
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₂