intro hij
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
⊢ Setoid.r i j → Fin.getRepr s i = Fin.getRepr s j
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
⊢ Fin.getRepr s i = Fin.getRepr s j