cases iv₁
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
hfst : iv₁.fst = iv₂.fst
hsnd : iv₁.snd = iv₂.snd
⊢ iv₁ = iv₂
case refine_3.mk
n : Nat
x : Permutation n
iv₂ : Inversion x
fst✝ snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hfst : { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.fst = iv₂.fst
hsnd : { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd = iv₂.snd
⊢ { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ } = iv₂