intro t
case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }),
    ∃ a,
      { 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]) } =
        b
case refine_2
n : Nat
x : Permutation n
t : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }
⊢ ∃ a,
    { 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]) } =
      t