unfold getRepr
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
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
⊢ (match h : Fin.find? fun b => decide (Setoid.r i b) with
    | some j =>
      let_fun this := ⋯;
      encodeSubtype (repr s) ⟨j, this⟩
    | none => absurd ⋯ ⋯) =
    match h : Fin.find? fun b => decide (Setoid.r j b) with
    | some j_1 =>
      let_fun this := ⋯;
      encodeSubtype (repr s) ⟨j_1, this⟩
    | none => absurd ⋯ ⋯