hooo_rev_imply is too strong ((a^c => b^c) => (a => b)^c)

[bvssvni]

// `(a => b)  =>  (b^a)`.
pub fn imply_to_pow<A: Prop, B: Prop>(ab: Imply<A, B>) -> Pow<B, A> {
    let x = pow_to_imply(tauto_pow_imply);
    let x = hooo_rev_imply(x);
    x(True)(ab)
}

This should not be provable.

- pow_to_imply (ok)
- tauto_pow_imply (ok)
  - pow_lift (ok)
  - tauto_imply_to_pow (ok)
    - hooo_imply (ok)
    - pow_lift (ok)
- hooo_rev_imply

The only weak point is hooo_rev_imply.