Function dependent_ghost::proof::equiv_elim

pub fn equiv_elim<P, Q>(_: Proof<Equiv<P, Q>>, _: Proof<P>) -> Proof<Q>