Commit 2022-06-09 05:43 971a9b00

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.