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).
(g . f) ⋀ (g == h) => (h . f)