coq

coq copied to clipboard

Universes u v.
Constraint u < v. (* or v < u *)
Axiom X : Type@{u} = Type@{v}.

Lemma foo : forall (P : Type@{u}) (p1 p2 : P), p1 = p2.
Proof.
  destruct X.
(* Error: Universe inconsistency. Cannot enforce v = u because u < v. *)

I believe this should succeed without a goal change.