hooo_dual_imply is too strong (c^(a => b) => ¬(c^b => c^a))

[bvssvni]

pub fn proof<A: Prop, B: Prop>(
    pow_ba: Pow<B, A>,
    pow_bna: Pow<B, Not<A>>
) -> False {
    pow_rev_not(pow_bna)(pow_ba)
}

pub fn proof2() -> False {
    fn f(_: Or<True, Not<True>>) -> True {True}
    let (a, b) = hooo_dual_or(f);
    proof(a, b)
}

Here, hooo_dual_or has a trusted proof:

/// `c^(a ⋁ b) => (c^a ⋀ c^b)`.
pub fn hooo_dual_or<A: Prop, B: Prop, C: Prop>(
    x: Pow<C, Or<A, B>>
) -> And<Pow<C, A>, Pow<C, B>> {
    (pow_transitivity(Left, x.clone()), pow_transitivity(Right, x))
}

The only weakness is hooo_dual_imply, used in pow_rev_not:

/// `a^(¬b) => ¬a^b`.
pub fn pow_rev_not<A: Prop, B: Prop>(x: Pow<A, Not<B>>) -> Not<Pow<A, B>> {
    let y = hooo_dual_imply(x);
    Rc::new(move |pow_a_b| {
        y(pow_a_b.map_any())
    })
}

[bvssvni]

This undermines the dual axiom scheme for HOOO EP.

[bvssvni]

This also implies tauto_hooo_dual_imply is too strong, since tauto_hooo_dual_imply implies hooo_dual_imply.