Commit 2022-09-26 05:32 3b4e9d58

feat(data/option/basic): option.map is injective (#16626)

• prove that option.map : (α → β) → (option α → option β) is injective;
• add iff version of this lemma;
• add option.map_comp_some and option.map_eq_id;
• drop option.map_id': it was the same as option.map_id.