Given a theorem-tactic ttac, a term u and a goal (A,t),
FILTER_STRIP_THEN ttac u removes one outer connective (!, ==>, or ~)
from t, if the term being stripped does not contain a free instance of u.
Note that FILTER_PSTRIP_THEN will strip paired universal quantifiers.
A negation ~t is treated as the implication t ==> F. The theorem-tactic
ttac is applied only when stripping an implication, by using the antecedent
stripped off. FILTER_PSTRIP_THEN also breaks conjunctions.
FILTER_PSTRIP_THEN behaves like PSTRIP_GOAL_THEN, if the term
being stripped does not contain a free instance of u. In particular,
FILTER_PSTRIP_THEN PSTRIP_ASSUME_TAC behaves like FILTER_PSTRIP_TAC.