Function prop::fun::comp_in_left_arg

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

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