basic): add `eq_of_mem_of_mem` (#11098)

Commit

3 years ago

feat(data/option/basic): add `eq_of_mem_of_mem` (#11098) If `a : α` belongs to both `o1 o2 : option α` then `o1 = o2`

Author

stuart-presnell

Parents