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