Make sensible implicit choices in :addlemma

Specifically, make an argument implicit if it's constructor guarded
elsewhere in the type (i.e. can be inferred by unification in the usual
way).