cases 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₂
case refine_3.mk.mk
n : Nat
x : Permutation n
fst✝¹ snd✝¹ : Fin n
lt✝¹ : fst✝¹ < snd✝¹
inverted✝¹ : x[↑fst✝¹] > x[↑snd✝¹]
fst✝ snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hfst :
  { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.fst =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.fst
hsnd :
  { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.snd =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }