feat(set_theory/cardinal,*): assorted lemmas (#9516)
### New instances
* a denumerable type is infinite;
* `Prop` is (noncomputably) enumerable;
* `Prop` is nontrivial;
* `cardinal.can_lift_cardinal_Type`: lift `cardinal.{u}` to `Type u`.
### New lemmas / attrs
* `quotient.out_equiv_out` : `x.out ≈ y.out ↔ x = y`;
* `quotient.out_inj` : `x.out = y.out ↔ x = y`;
* `cardinal.lift_bit0`, `cardinal.lift_bit1`, `cardinal.lift_two`, `cardinal.lift_prod` :
new lemmas about `cardinal.lift`;
* `cardinal.omega_le_lift` and `cardinal.lift_le_omega` : simplify `ω ≤ lift c` and `lift c ≤ ω`;
* `cardinal.omega_le_add_iff`, `cardinal.encodable_iff`, `cardinal.mk_le_omega`,
`cardinal.mk_denumerable`: new lemmas about `cardinal.omega`;
* add `@[simp]` attribute to `cardinal.mk_univ`, add `cardinal.mk_insert`;
* generalize `cardinal.nat_power_eq` to `cardinal.power_eq_two_power` and `cardinal.prod_eq_two_power`.
