[Agda] new generalize feature, first version

[Nils Anders Danielsson]

On 2018-04-01 20:04, Peter Divianszky wrote:
> Yes, it seems that Coq also has a forall-generalisation. The main
> difference is that it is not possible to specify the types of the
> variables to be generalized.

Correct me if I'm wrong, but I don't think Coq has a first-class
implicit function space like Agda does. (This function space has led to
a number of problems.)

-- 
/NAD