STRIP_THM_THEN : thm_tactical
ttac(u |- u) THEN ttac(v |- v)
A ?- t A ?- t ========= ttac (u |- u) and ========= ttac (v |- v) A ?- t1 A ?- t2
A ?- t ================== STRIP_THM_THEN ttac (A' |- u \/ v) A ?- t1 A ?- t2
A ?- t ========= ttac (u |- u) A ?- t1
A ?- t ============= STRIP_THM_THEN ttac (A' |- ?x. u) A ?- t1