sig
  val eq_refl : Term.types -> Term.constr -> Term.constr
  val eq : Term.types -> Term.constr
end