Module Coq.Leibniz

module Leibniz: sig .. end

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