mathlib3

971a9b00 - feat(logic/equiv/basic): two empty types are equivalent; remove various redundant lemmas (#14604)

feat(logic/equiv/basic): two empty types are equivalent; remove various redundant lemmas (#14604) We prove `equiv_of_is_empty`, which states two empty types are equivalent. This allows us to remove various redundant lemmas. We keep `empty_equiv_empty` and `empty_equiv_pempty` as these specific instantiations of that lemma are widely used.