The Coq mailing list

[James Tyler <jameskatyler AT gmail.com>]

I am not sure why this is valid:

  Definition AProp {A : Set} (Q : A -> Prop) : Set :=
    forall x : A, Q x.
  Check AProp.
  (* Output : (?9 -> Prop) -> Set *)
  Check forall {A : Set} (Q : A -> Prop) (x : A), Q x.
  (* Output : Prop *)

Does this have something to do with Definitions being opaque? According 
to the triplets on Pg. 92 of Coq'Art, I shouldn't be allowed to do this. 
I stumbled upon this and I'm not entirely sure why one would want to do 
it either. Thoughts?