simplify ProgramClauseImplication

[nikomatsakis]

Currently we have the ProgramClause type, which maps to an enum ProgramClauseData with two options:

• Implies -- a ProgramClauseImplication, corresponding to P :- Q1..Qn (i.e., P is true if Q1...Qn are provable)
• ForAll -- which wraps the same ProgramClauseImplication in binders, corresponding to forall<...> { P :- Q1..qn }.

I think we should remove the Implies variant and just have that a ProgramClause maps to a Binders<ProgramClauseImplication>, but those binders may be empty.

This is a straight refactoring and simplification.

This issue has been assigned to @declanvk via this comment.

[declanvk]

@rustbot claim

Edit: Is it alright if I grab this?