compose [nat] sterm [with sterm] [intros-spec]

Composes t1 with t2 in every possible way n times introducing generated terms as if intros hyps was issued.

If t1:∀x:A.B[x] and t2:∀x,y:A.B[x]→B[y]→C[x,y] it generates:

If t2 is omitted it composes t1 with every hypothesis that can be introduced. n iterates the process.

The same, but with more hypothesis eventually introduced by the intros-spec.