FStar.Witnessed.Core: mark witnessed argument as @@@unused

This allows to user a witnessed token in recursive definitions in
non-strictly positive positions. The justification is
1) that this token is really just a unit, it's the axiom that gives it
any interesting behavior, and
2) that this token cannot be used except through an effectful operation.

So it should be safe to mark it its type argument @@@unused.

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
 

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