Tries to weaken the conclusion of a theorem consisting of an
implication.
DESCRIPTION
Given a theorem of the form |- A ==> C and a directed consequence
conversion c a call of WEAKEN_CONSEQ_CONV_RULE c thm tries to
weaken C to a predicate wC using c. If it succeeds it returns
the theorem |- A ==> wC.