STRIP_TAC : tactic
A ?- !x.u ============== STRIP_TAC A ?- u[x'/x]
A ?- v /\ w ================= STRIP_TAC A ?- v A ?- w
A ?- v1 /\ ... /\ vn ==> v A ?- v1 \/ ... \/ vn ==> v ============================ ================================= A u {v1,...,vn} ?- v A u {v1} ?- v ... A u {vn} ?- v A ?- ?x.w ==> v ==================== A u {w[x'/x]} ?- v
# g `!m n. m <= n /\ n <= m ==> m = n`;;
# e(REPEAT STRIP_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`m <= n`] 1 [`n <= m`] `m = n`