The Coq mailing list

["sdk" <sdk AT mathink.net>]

Maybe, let-in and {} may be able to solve half of the problem.

I don't know how to write like:

Definition D1 : Type := forall {T: Type}(x: T), Type.

and I checked that command 'Arguments D1 {T}(x).' rejected.

But, e.g. in definition of DD1, using let-in and {} enable to write A x
instead of A T x:

Definition DD1 ( A0 : D1 ) :=
  let A {T:Type}(x: T) := A0 T x in (A 1, A true).

It seems ad-hoc, but I don't have any idea now.

If there is many functions such as DD1, many lets will be needed...