Tactical.PRED

PRED_ASSUM finds the first assumption satisfying the prediate given, removes it from the assumption list, ASSUMEs it, passes it to the theorem-tactic and then applies the consequent tactic. Thus, where t is the first assumption satisfying p,

   PRED_ASSUM p f ([a1,... ai, t, aj, ... an], goal) =
     f (ASSUME t) ([a1,... ai, aj,... an], goal)

For example (again, where t is the first assumption in A u {t} satisfying p), if

    A ?- c
   ========  f (ASSUME t)
    B ?- v

then

    A u {t} ?- c
   ===============  PRED_ASSUM p f
       B ?- v