feat(data/quot.lean): add lift_on_beta\_2 (#3456)
This corresponds to `lift_on\_2` in `library/init/data/quot.lean` just as `lift_beta` and `lift_on_beta` correspond to `lift` and `lift_on`. It greatly simplifies quotient proofs but was, surprisingly, missing.
