Matita Home

`compose n t1 with t2 hyps`

- Synopsis:
**compose**[*nat*]*sterm*[**with***sterm*] [*intros-spec*]- Pre-conditions:
- Action:
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*.