suffices x.inversions.Nodup ∧ ∀ iv, iv ∈ x.inversions → iv.snd.1 < n
from this.1
n : Nat
x : Permutation n
⊢ Array.Nodup (inversions x)
n : Nat
x : Permutation n
⊢ Array.Nodup (inversions x) ∧ ∀ (iv : Inversion x), iv ∈ inversions x → ↑iv.snd < n