Modified proofs for new claset primitives. The problem is that they enforce
the "most recent added rule has priority" policy more strictly now.
(*Dummy theory to document dependencies *)
Datatype = "constructor" + Inductive + Univ + QUniv
(*Datatype must be capital to avoid conflicts with ML's "datatype" *)