tauto_hooo_rev_imply is too strong ((a^c => b^c)^true => (a => b)^c)

[bvssvni]

It is possible to prove hooo_rev_imply using tauto_hooo_rev_imply:

pub fn hooo_rev_imply<A: Prop, B: Prop, C: Prop>(
    x: Imply<Pow<A, C>, Pow<B, C>>
) -> Pow<Imply<A, B>, C> {
    fn f<A: Prop, B: Prop, C: Prop>(_: True) ->
        Imply<Tauto<Imply<Pow<A, C>, Pow<B, C>>>, Tauto<Pow<Imply<A, B>, C>>> {
        Rc::new(move |x| pow_lift(tauto_hooo_rev_imply(x)))
    }
    tauto_hooo_rev_imply(f)(True)(x)
}

hooo_rev_imply is too strong, see #640