Commit 2023-12-07 16:10 8289b55e
View on Github →chore(Order/RelIso): drop a duplicate lemma (#2390)
Duplicate of coe_fn_toEquiv
several lines below.
chore(Order/RelIso): drop a duplicate lemma (#2390)
Duplicate of coe_fn_toEquiv
several lines below.