TRANS_TAC : thm -> term -> tactic
|- !xs. R1 x y /\ R2 y z ==> R3 x z
A ?- R3 s u ======================== TRANS_TAC (|- !xs. R1 x y /\ R2 y z ==> R3 x z) `t` A ?- R1 s t /\ R2 t u
# g `n < (m + 2) * (n + 1)`;;
# LET_TRANS;; val it : thm = |- !m n p. m <= n /\ n < p ==> m < p
# e(TRANS_TAC LET_TRANS `1 * (n + 1)`);; val it : goalstack = 1 subgoal (1 total) `n <= 1 * (n + 1) /\ 1 * (n + 1) < (m + 2) * (n + 1)`