1 files changed, 2 insertions, 0 deletions
diff --git a/coq.ml b/coq.ml
index 7371913..132fbf7 100644
--- a/coq.ml
+++ b/coq.ml
@@ -148,6 +148,8 @@ module Leibniz = struct
   let path = ["Coq"; "Init"; "Logic"]
   let eq_refl = lazy (init_constant path "eq_refl")
   let eq_refl ty x = lapp eq_refl [| ty;x|]
+  let eq ty = Term.mkApp (init_constant path "eq", [| ty |])
+
 end
 
 module Option = struct