ASM_CASES_TAC : term -> tactic
A ?- t ================================ ASM_CASES_TAC `u` A u {u} ?- t A u {~u} ?- t
# g `&0 <= (u:real) pow 2`;; Warning: Free variables in goal: u val it : goalstack = 1 subgoal (1 total) `&0 <= u pow 2` # e(ASM_CASES_TAC `&0 <= u`);; val it : goalstack = 2 subgoals (2 total) 0 [`~(&0 <= u)`] `&0 <= u pow 2` 0 [`&0 <= u`] `&0 <= u pow 2`