refactor(data/option/defs): Swap arguments to `option.elim` (#14681)
Make `option.elim` a non-dependent version of `option.rec` rather than a non-dependent version of `option.rec_on`. Same for `option.melim`.
This replaces `option.cons`, and brings `option.elim` in line with `nat.elim`, `sum.elim`, and `iff.elim`.
It addresses the TODO comment added in 22c4291217925c6957c0f5a44551c9917b56c7cf.