weakening rule

This rule already appears in elaborated proofs output by Carcara.

@bandreotti writes: Takes a clause as a premise, and concludes that clause with one or more terms added at the end. May be added by Carcara when elaborating eq_transitive or resolution steps.

This rule (or an alternative formulation that Carcara can use instead) should be added to the standard. @bandreotti has more information about the formal description of the rule.

(we decided to rename the or_intro rule to weakening, see below)