A strange behaviour in Coq

The files "one" and "two" below can be required alone, but not together, due to a cycle in the universe constraints:

   file definitions.v 
    Definition P := Type -> Type. 
    Definition Q := Type -> Type. 
    Definition p : P := [x:Type]x. 
    Definition q : Q := [x:Type]x. 

   file one.v 
    Require definitions. 
    Theorem easy1 : (a : (p Q))True. 
    Auto. 
    Qed. 

   file two.v 
    Require definitions. 
    Theorem easy2 : (a : (q P))True. 
    Auto. 
    Qed.