[Agda] new generalize feature, first version

[Jannis Limperg]

Agda's unnamed modules are closer to Coq's sections than this new
feature, working pretty much exactly like Joachim describes. Hence, I
would also find 'sections' confusing.

For the same reason, I don't like 'notation' too much, since it invokes
Coq's notation feature, which is Agda's 'syntax' on steroids. Of course,
it is not exactly an absolute imperative that Agda stay consistent with
Coq's usage of these terms, but it's something to consider.

Peter's new feature, if I understand it correctly, is closest to Coq's
implicit generalization [1, Section 2.7.19] (which is frequently handy,
so add my voice to the choir of fans of this feature.) To summarise
Coq's design:

- You can declare variable names as generalizable using `Generalizable
Variables x y z` or `Generalizable All Variables`. This roughly
corresponds to Peter's `generalize` declaration.
- Contrary to Peter's design, generalization only takes effect if the
generalizable variables are mentioned in a special binder that enables
generalization, of the form `(P : n = n) or `{P : n = n} (the backtick
is part of the binder). Given the above binders, n would be generalized
if it was previously declared generalizable. I have no strong opinion on
requiring this additional step; perhaps one could ask on Coq-Club why
the Coq implementors chose to do so.

An example:

    Generalizable Variables A.

    Definition id `(x : A) : A := x.

    About id.

    (* id : forall A : Type, A -> A

      Argument A is implicit and maximally inserted [...] *)

[1] https://coq.inria.fr/refman/gallina-ext.html#Implicit%20Arguments