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