Eta contract solutions

[gares]

No description provided.

[FissoreD]

I tried these commits on my branch, but it seems to break some tests. In particular I get an error like:

The term "s" has type
 "forall M : Type@{s.u0} -> Type@{s.u1},
  (forall A : Type@{s.u0}, Singleton1 (M A)) -> forall A : Type@{s.u2}, Singleton (M A)"
while it is expected to have type
 "forall M : Type@{Unnamed_thm.u0} -> Type@{Unnamed_thm.u1},
  (forall A : Type@{Unnamed_thm.u0}, Singleton1 (M A)) ->
  forall A : Type@{Unnamed_thm.u2}, Singleton (M A)".

In fact the solution of my goal is found correct: I expect it finds s and it does,
but when I Qed the proof, it seems there are problems in universes...