diff --git a/ulib/experimental/FStar.Witnessed.Core.fst b/ulib/experimental/FStar.Witnessed.Core.fst
index f51a82b105b..f91442690cf 100644
--- a/ulib/experimental/FStar.Witnessed.Core.fst
+++ b/ulib/experimental/FStar.Witnessed.Core.fst
@@ -6,7 +6,7 @@ module P = FStar.Preorder
    
 let witnessed (state:Type u#a)
               (rel:P.preorder state)
-              (p:s_predicate state)
+              ([@@@unused] p:s_predicate state)
   : Type0
   = unit
   
diff --git a/ulib/experimental/FStar.Witnessed.Core.fsti b/ulib/experimental/FStar.Witnessed.Core.fsti
index 50fcaa61ce9..63191572a41 100644
--- a/ulib/experimental/FStar.Witnessed.Core.fsti
+++ b/ulib/experimental/FStar.Witnessed.Core.fsti
@@ -10,7 +10,7 @@ let stable (state:Type u#a)
 
 val witnessed (state:Type u#a)
               (rel:P.preorder state)
-              (p:s_predicate state)
+              ([@@@unused] p:s_predicate state)
   : Type0
 
 val witnessed_proof_irrelevant