Function comp_is_const 

pub fn comp_is_const<F: Prop, G: Prop>(
    a: IsConst<F>,
    b: IsConst<G>,
) -> IsConst<Comp<G, F>>

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