Function dependent_ghost::proof::impl_intro

pub fn impl_intro<P, Q, F>(_: F) -> Proof<Implies<P, Q>> where
    F: Fn(Proof<P>) -> Proof<Q>,