as if <command>intros hyps</command> was issued.</para>
<para>If <command>t1:∀x:A.B[x]</command> and
<command>t2:∀x,y:A.B[x]→B[y]→C[x,y]</command> it generates:
as if <command>intros hyps</command> was issued.</para>
<para>If <command>t1:∀x:A.B[x]</command> and
<command>t2:∀x,y:A.B[x]→B[y]→C[x,y]</command> it generates: