Commit 2018-09-10 22:44 0e069447
View on Github →feat(data/equiv/basic): quot_equiv_of_quot(') quot_equiv_of_quot matches matches the existing subtype_equiv_of_subtype, but quot_equiv_of_quot' is useful in practice and this definition is careful to use eq.rec only in proofs.