Function prop::eq::rev_modus_tollens

source ·
pub fn rev_modus_tollens<A: DProp, B: DProp>(
    (f0, f1): Eq<Not<A>, Not<B>>
) -> Eq<B, A>
Expand description

(¬a == ¬b) => (b == a).