clean
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
j' : Fin n
hj' : (Fin.find? fun b => decide (Setoid.r j b)) = some j'
⊢ (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨i', this⟩) =
    let_fun this := ⋯;
    encodeSubtype (repr s) ⟨j', this⟩
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
j' : Fin n
hj' : (Fin.find? fun b => decide (Setoid.r j b)) = some j'
⊢ encodeSubtype (repr s) ⟨i', ⋯⟩ = encodeSubtype (repr s) ⟨j', ⋯⟩