pub fn comp_assoc<F: Prop, G: Prop, H: Prop>( ) -> Eq<Comp<H, Comp<G, F>>, Comp<Comp<H, G>, F>>
h . (g . f) == (h . g) . f.
h . (g . f) == (h . g) . f