# 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.