Commit 2020-07-10 04:14 c949dd45

chore(logic/embedding): reuse proofs from data.* (#3341) Other changes:

• rename injective.prod to injective.prod_map;
• add surjective.prod_map;
• redefine sigma.map without pattern matching;
• rename sigma_map_injective to injective.sigma_map;
• add surjective.sigma_map;
• add injective.sum_map and surjective.sum_map;
• rename embedding.prod_congr to embedding.prod_map;
• rename embedding.sum_congr to embedding.sum_map;
• delete embedding.sigma_congr_right, add more general embedding.sigma_map.