Module AAC_coq.Leibniz


module Leibniz: sig .. end

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