Function prop::fun::comp_eq_right

pub fn comp_eq_right<F: Prop, G: Prop, H: Prop>(
    x: Eq<G, H>
) -> Eq<Comp<F, G>, Comp<F, H>>

(g == h) => (f . g) == (f . h).