Commit 2022-06-09 13:27 d997baa4

refactor(logic/equiv/basic): remove fin_equiv_subtype (#14603) The types fin n and {m // m < n} are definitionally equal, so it doesn't make sense to have a dedicated equivalence between them (other than equiv.refl). We remove this equivalence and golf the places where it was used.