Function dependent_ghost::proof::and_elim_r

pub fn and_elim_r<P, Q>(_: Proof<And<P, Q>>) -> Proof<Q>