Generalization under implication by λ-subsumption