Commit 2021-08-26 10:02 058f639e

feat(data/equiv/fin): fin_succ_equiv_last (#8805) This commit changes the type of fin_succ_equiv'. fin_succ_equiv' i used to take an argument of type fin n which was strange and it now takes an argument of type fin (n + 1) meaning it is now possible to send fin.last n to none if desired. I also defined fin.succ_equiv_last, the canonical equiv fin (n + 1) to option (fin n) sending fin.last to none.