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).