Function dependent_ghost::proof::equiv_intro

pub fn equiv_intro<P, Q, F1, F2>(_: F1, _: F2) -> Proof<Equiv<P, Q>> where
    F1: Fn(Proof<P>) -> Proof<Q>,
    F2: Fn(Proof<Q>) -> Proof<P>,