compose n t1 with t2 hyps


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:

  • λx,y:A.t2 x y (t1 x) : ∀x,y:A.B[y]→C[x,y]

  • λx,y:A.λH:B[x].t2 x y H (t1 y) : ∀x,y:A.B[x]→C[x,y]

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

New sequents to prove:

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