(THEN) : tactic -> tactic -> tactic
# g `!x y. (x INSERT s) DELETE y = if x = y then s DELETE y else x INSERT (s DELETE y)`;;
# e(REPEAT GEN_TAC);; val it : goalstack = 1 subgoal (1 total) `(x INSERT s) DELETE y = (if x = y then s DELETE y else x INSERT (s DELETE y))`
# e COND_CASES_TAC;; ...
# e(REPEAT GEN_TAC THEN COND_CASES_TAC);; ...
EQ_TAC THENL [ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]]
EQ_TAC THEN ASM_REWRITE_TAC[]