Apply with x
It should be possible to give hint terms to apply (or rewrite). For example: "apply h with x,y"
For example, it should allow to directly apply a lemma on transitivity:
"H : forall x y z, x < y -> y < z -> x < z
Goal: 0 < 2"
"apply H with 1" generates two new goals "0 < 1" and "1 < 2"