To be precise, given a monoidal signature $S$ (i.e, a set of generating objects $O$ and morphisms with source and target taken in the free monoid over $O$) , we can generate the free Cartesian closed category over $S$, $CCC(S)$, which is such that for every CCC $C$ and interpretation function $i:S \to U(C)$, where $U: MonCat \to MonSig$ is the forgetful functor to the category of monoidal signatures, there exists a unique functor $[-]_i: CCC(S) \to C$ such that $i = U([-]_i) \circ j$, where $j: S \to U(CCC(S))$ is the obvious inclusion.
Then my question is if the following holds for every parallel pair of morphisms (i.e., lambda terms) $f$ and $g$ in $CCC(S)$: if for every interpretation function $i:S \to U(Set)$ we have $[f]_i = [g]_i$, then $f = g$.
I have found results in the literature which prove this is the case for a simple signature (i.e., a monoidal signature with no generating morphisms). I want to know if this is the case when generating morphisms are included in the signature, and if so where can I reference this fact? Or is it a simple extension of an existing proof for the simple case?
