intro hfst hsnd
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
⊢ iv₁.fst = iv₂.fst → iv₁.snd = iv₂.snd → iv₁ = 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₂