REPEAT : tactic -> tactic
# g `!w x y z. w < z /\ x < y ==> w * x + 1 <= y * z`;;
# e GEN_TAC;; val it : goalstack = 1 subgoal (1 total) `!x y z. w < z /\ x < y ==> w * x + 1 <= y * z`
# e(REPEAT GEN_TAC);; val it : goalstack = 1 subgoal (1 total) `w < z /\ x < y ==> w * x + 1 <= y * z`