Function dependent_ghost::proof::modus_ponens

pub fn modus_ponens<P, Q>(f: Proof<Implies<P, Q>>, x: Proof<P>) -> Proof<Q>