diff --git a/flake.lock b/flake.lock
index 0e28b8a..8404759 100644
--- a/flake.lock
+++ b/flake.lock
@@ -36,11 +36,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1722599947,
-        "narHash": "sha256-/vyB45kDyp6XlbJFVldw95QDKkmrwbet8VM6VoVNw6M=",
+        "lastModified": 1723666324,
+        "narHash": "sha256-e63avv7rUj6M5mnQ3E0aK/UsWWTDppQu7nlBeeTyRNI=",
         "owner": "REPROSEC",
         "repo": "dolev-yao-star-extrinsic",
-        "rev": "170ed7e9aa94199f11f83d533a73bd9330d92675",
+        "rev": "b0af94f53f5ece72d51353bd90b2b65b68f1ad56",
         "type": "github"
       },
       "original": {
diff --git a/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst b/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
index d84f660..d5f2b0c 100644
--- a/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
+++ b/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
@@ -59,7 +59,7 @@ let split_signwithlabel_crypto_pred_params {|crypto_usages|}: split_function_par
 }
 
 #push-options "--ifuel 1"
-val has_signwithlabel_pred: {|cusgs:crypto_usages|} -> sign_crypto_predicate cusgs -> (valid_label & signwithlabel_crypto_pred) -> prop
+val has_signwithlabel_pred: {|crypto_usages|} -> sign_crypto_predicate -> (valid_label & signwithlabel_crypto_pred) -> prop
 let has_signwithlabel_pred #cusgs sign_pred (lab, local_pred) =
   forall tr vk msg.
     {:pattern sign_pred.pred tr vk msg}
@@ -74,8 +74,8 @@ let has_signwithlabel_pred #cusgs sign_pred (lab, local_pred) =
 #pop-options
 
 val intro_has_signwithlabel_pred:
-  {|cusgs:crypto_usages|} ->
-  sign_pred:sign_crypto_predicate cusgs -> tagged_local_pred:(valid_label & signwithlabel_crypto_pred) ->
+  {|crypto_usages|} ->
+  sign_pred:sign_crypto_predicate -> tagged_local_pred:(valid_label & signwithlabel_crypto_pred) ->
   Lemma
   (requires has_local_fun split_signwithlabel_crypto_pred_params sign_pred.pred tagged_local_pred)
   (ensures has_signwithlabel_pred sign_pred tagged_local_pred)
@@ -123,9 +123,9 @@ let mk_global_mls_sign_pred_later tagged_local_preds tr1 tr2 vk msg =
 #pop-options
 
 val mk_mls_sign_pred:
-  {|cusgs:crypto_usages|} ->
+  {|crypto_usages|} ->
   list (valid_label & signwithlabel_crypto_pred) ->
-  sign_crypto_predicate cusgs
+  sign_crypto_predicate
 let mk_mls_sign_pred #cusgs tagged_local_preds = {
   pred = mk_global_mls_sign_pred tagged_local_preds;
   pred_later = mk_global_mls_sign_pred_later tagged_local_preds;
@@ -133,15 +133,15 @@ let mk_mls_sign_pred #cusgs tagged_local_preds = {
 
 #push-options "--ifuel 1"
 val mk_mls_sign_pred_correct:
-  {|cusgs:crypto_usages|} ->
-  sign_pred:sign_crypto_predicate cusgs -> tagged_local_preds:list (valid_label & signwithlabel_crypto_pred) ->
+  {|crypto_usages|} ->
+  sign_pred:sign_crypto_predicate -> tagged_local_preds:list (valid_label & signwithlabel_crypto_pred) ->
   Lemma
   (requires
     sign_pred == mk_mls_sign_pred tagged_local_preds /\
     List.Tot.no_repeats_p (List.Tot.map fst tagged_local_preds)
   )
   (ensures for_allP (has_signwithlabel_pred sign_pred) tagged_local_preds)
-let mk_mls_sign_pred_correct sign_pred tagged_local_preds =
+let mk_mls_sign_pred_correct #cusgs sign_pred tagged_local_preds =
   for_allP_eq (has_signwithlabel_pred sign_pred) tagged_local_preds;
   no_repeats_p_implies_for_all_pairsP_unequal (List.Tot.map fst tagged_local_preds);
   FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_signwithlabel_crypto_pred_params tagged_local_preds));
@@ -153,7 +153,7 @@ let mk_mls_sign_pred_correct sign_pred tagged_local_preds =
 val has_mls_signwithlabel_pred: {|crypto_invariants|} -> (valid_label & signwithlabel_crypto_pred) -> prop
 let has_mls_signwithlabel_pred #cinvs tagged_local_pred =
   exists mls_sign_pred.
-    has_sign_predicate cinvs ("MLS.LeafSignKey", mls_sign_pred) /\
+    has_sign_predicate ("MLS.LeafSignKey", mls_sign_pred) /\
     has_signwithlabel_pred mls_sign_pred tagged_local_pred
 
 (*** Lemmas on SignWithLabel and VerifyWithLabel ***)
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst
index be7f0ac..6d7d5d6 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst
@@ -40,9 +40,9 @@ let group_manager_pred #ci = {
   pred_knowable = (fun tr prin state_id key value -> ());
 }
 
-val has_group_manager_invariant: protocol_invariants -> prop
-let has_group_manager_invariant invs =
-  has_map_session_invariant invs group_manager_pred
+val has_group_manager_invariant: {|protocol_invariants|} -> prop
+let has_group_manager_invariant #invs =
+  has_map_session_invariant group_manager_pred
 
 val group_manager_tag_and_invariant: {|crypto_invariants|} -> string & local_bytes_state_predicate
 let group_manager_tag_and_invariant #ci = (group_manager_types.tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant group_manager_pred))
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst
index 26f120a..47b1ef9 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst
@@ -35,9 +35,9 @@ let key_package_manager_pred #ci tkt = {
   );
 }
 
-val has_key_package_manager_invariant: treekem_types dy_bytes -> protocol_invariants -> prop
-let has_key_package_manager_invariant tkt invs =
-  has_map_session_invariant invs (key_package_manager_pred tkt)
+val has_key_package_manager_invariant: treekem_types dy_bytes -> {|protocol_invariants|} -> prop
+let has_key_package_manager_invariant tkt #invs =
+  has_map_session_invariant (key_package_manager_pred tkt)
 
 val key_package_manager_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> string & local_bytes_state_predicate
 let key_package_manager_tag_and_invariant #ci tkt = ((key_package_manager_types tkt).tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant (key_package_manager_pred tkt)))
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
index ea422fb..8c5d955 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
@@ -89,9 +89,9 @@ let treesync_public_state_pred #ci tkt = {
 instance local_state_bare_treesync_state (tkt:treekem_types dy_bytes): local_state (bare_treesync_state tkt) =
   mk_local_state_instance "MLS.TreeSync.PublicState"
 
-val has_treesync_public_state_invariant: treekem_types dy_bytes -> protocol_invariants -> prop
-let has_treesync_public_state_invariant tkt invs =
-  has_local_state_predicate invs (treesync_public_state_pred tkt)
+val has_treesync_public_state_invariant: treekem_types dy_bytes -> {|protocol_invariants|} -> prop
+let has_treesync_public_state_invariant tkt #invs =
+  has_local_state_predicate (treesync_public_state_pred tkt)
 
 val treesync_public_state_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> string & local_bytes_state_predicate
 let treesync_public_state_tag_and_invariant #ci tkt = ((local_state_bare_treesync_state tkt).tag, local_state_predicate_to_local_bytes_state_predicate (treesync_public_state_pred tkt))
@@ -120,7 +120,7 @@ let new_public_treesync_state #tkt #group_id prin st =
   return state_id
 
 val new_public_treesync_state_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> 
   prin:principal ->
   st:treesync_state dy_bytes tkt dy_as_token group_id ->
@@ -131,7 +131,7 @@ val new_public_treesync_state_proof:
     is_well_formed _ (is_publishable tr) (st.tree <: treesync _ _ _ _) /\
     treesync_state_valid (dy_asp tr) st /\
     trace_invariant tr /\
-    has_treesync_public_state_invariant tkt invs
+    has_treesync_public_state_invariant tkt
   )
   (ensures (
     let (_, tr_out) = new_public_treesync_state prin st tr in
@@ -148,7 +148,7 @@ let set_public_treesync_state #tkt #group_id prin state_id st =
   set_state prin state_id (treesync_state_to_bare_treesync_state st)
 
 val set_public_treesync_state_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes ->
   prin:principal -> state_id:state_id ->
   st:treesync_state dy_bytes tkt dy_as_token group_id ->
@@ -159,7 +159,7 @@ val set_public_treesync_state_proof:
     is_well_formed _ (is_publishable tr) (st.tree <: treesync _ _ _ _) /\
     treesync_state_valid (dy_asp tr) st /\
     trace_invariant tr /\
-    has_treesync_public_state_invariant tkt invs
+    has_treesync_public_state_invariant tkt
   )
   (ensures (
     let ((), tr_out) = set_public_treesync_state prin state_id st tr in
@@ -184,14 +184,14 @@ let get_public_treesync_state #tkt prin state_id =
   } <: treesync_state dy_bytes tkt dy_as_token bare_st.group_id)|))
 
 val get_public_treesync_state_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   prin:principal -> state_id:state_id ->
   tr:trace ->
   Lemma
   (requires
     trace_invariant tr /\
-    has_treesync_public_state_invariant tkt invs
+    has_treesync_public_state_invariant tkt
   )
   (ensures (
     let (opt_result, tr_out) = get_public_treesync_state prin state_id tr in
@@ -231,9 +231,9 @@ let treesync_private_state_pred #ci = {
 instance local_state_treesync_private_state: local_state treesync_private_state =
   mk_local_state_instance "MLS.TreeSync.PrivateState"
 
-val has_treesync_private_state_invariant: protocol_invariants -> prop
-let has_treesync_private_state_invariant invs =
-  has_local_state_predicate invs treesync_private_state_pred
+val has_treesync_private_state_invariant: {|protocol_invariants|} -> prop
+let has_treesync_private_state_invariant #invs =
+  has_local_state_predicate treesync_private_state_pred
 
 val treesync_private_state_tag_and_invariant: {|crypto_invariants|} -> string & local_bytes_state_predicate
 let treesync_private_state_tag_and_invariant #ci = (local_state_treesync_private_state.tag, local_state_predicate_to_local_bytes_state_predicate treesync_private_state_pred)
@@ -249,14 +249,14 @@ let new_private_treesync_state prin st =
   return state_id
 
 val new_private_treesync_state_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   prin:principal -> st:treesync_private_state ->
   tr:trace ->
   Lemma
   (requires
     is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key /\
     trace_invariant tr /\
-    has_treesync_private_state_invariant invs
+    has_treesync_private_state_invariant
   )
   (ensures (
     let (_, tr_out) = new_private_treesync_state prin st tr in
@@ -271,14 +271,14 @@ let set_private_treesync_state prin state_id st =
   set_state prin state_id st
 
 val set_private_treesync_state_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   prin:principal -> state_id:state_id -> st:treesync_private_state ->
   tr:trace ->
   Lemma
   (requires
     is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key /\
     trace_invariant tr /\
-    has_treesync_private_state_invariant invs
+    has_treesync_private_state_invariant
   )
   (ensures (
     let ((), tr_out) = set_private_treesync_state prin state_id st tr in
@@ -293,13 +293,13 @@ let get_private_treesync_state prin state_id =
   get_state prin state_id
 
 val get_private_treesync_state_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   prin:principal -> state_id:state_id ->
   tr:trace ->
   Lemma
   (requires
     trace_invariant tr /\
-    has_treesync_private_state_invariant invs
+    has_treesync_private_state_invariant
   )
   (ensures (
     let (opt_result, tr_out) = get_private_treesync_state prin state_id tr in
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
index 6040dd6..e65857f 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
@@ -44,14 +44,14 @@ let extract_result #a x =
   | MLS.Result.ProtocolError s -> return None
 #pop-options
 
-val has_treesync_invariants: treekem_types dy_bytes -> protocol_invariants -> prop
-let has_treesync_invariants tkt invs =
-  has_treesync_public_state_invariant tkt invs /\
-  has_treesync_private_state_invariant invs /\
-  has_group_manager_invariant invs /\
-  has_key_package_manager_invariant tkt invs /\
-  has_as_cache_invariant invs /\
-  has_leaf_node_tbs_invariant tkt invs.crypto_invs
+val has_treesync_invariants: treekem_types dy_bytes -> {|protocol_invariants|} -> prop
+let has_treesync_invariants tkt #invs =
+  has_treesync_public_state_invariant tkt /\
+  has_treesync_private_state_invariant /\
+  has_group_manager_invariant /\
+  has_key_package_manager_invariant tkt /\
+  has_as_cache_invariant /\
+  has_leaf_node_tbs_invariant tkt
 
 val get_token_for:
   p:principal -> as_session:state_id ->
@@ -63,14 +63,14 @@ let get_token_for p as_session (verification_key, credential) =
   return (Some ({ who; time; } <: dy_as_token))
 
 val get_token_for_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   p:principal -> as_session:state_id ->
   inp:as_input dy_bytes ->
   tr:trace ->
   Lemma
   (requires
     trace_invariant tr /\
-    has_as_cache_invariant invs
+    has_as_cache_invariant
   )
   (ensures (
     let (opt_token, tr_out) = get_token_for p as_session inp tr in
@@ -83,7 +83,7 @@ val get_token_for_proof:
     )
   ))
   [SMTPat (get_token_for p as_session inp tr);
-   SMTPat (has_as_cache_invariant invs)]
+   SMTPat (has_as_cache_invariant)]
 let get_token_for_proof #invs p as_session (verification_key, credential) tr = ()
 
 #push-options "--fuel 1 --ifuel 1"
@@ -109,14 +109,14 @@ let rec get_tokens_for p as_session inps =
 
 #push-options "--fuel 1 --ifuel 1"
 val get_tokens_for_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   p:principal -> as_session:state_id ->
   inps:list (option (as_input dy_bytes)) ->
   tr:trace ->
   Lemma
   (requires
     trace_invariant tr /\
-    has_as_cache_invariant invs
+    has_as_cache_invariant
   )
   (ensures (
     let (opt_tokens, tr_out) = get_tokens_for p as_session inps tr in
@@ -135,7 +135,7 @@ val get_tokens_for_proof:
     )
   ))
   [SMTPat (get_tokens_for p as_session inps tr);
-   SMTPat (has_as_cache_invariant invs)]
+   SMTPat (has_as_cache_invariant)]
 let rec get_tokens_for_proof #invs p as_session inps tr =
   match inps with
   | [] -> ()
@@ -161,7 +161,7 @@ let create #tkt p as_session gmgr_session group_id ln secret_session =
   return (Some ())
 
 val create_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   p:principal -> as_session:state_id -> gmgr_session:state_id ->
   group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> secret_session:state_id ->
@@ -171,7 +171,7 @@ val create_proof:
     is_publishable tr group_id /\
     is_well_formed _ (is_publishable tr) ln /\
     trace_invariant tr /\
-    has_treesync_invariants tkt invs
+    has_treesync_invariants tkt
   )
   (ensures (
     let (_, tr_out) = create p as_session gmgr_session group_id ln secret_session tr in
@@ -208,7 +208,7 @@ let welcome #tkt p as_session gmgr_session kpmgr_session my_key_package group_id
   add_new_group_sessions p gmgr_session { group_id } group_sessions
 
 val welcome_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   p:principal -> as_session:state_id -> gmgr_session:state_id -> kpmgr_session:state_id ->
   my_key_package:key_package_nt dy_bytes tkt ->
@@ -219,7 +219,7 @@ val welcome_proof:
     is_publishable tr group_id /\
     is_well_formed _ (is_publishable tr) t /\
     trace_invariant tr /\
-    has_treesync_invariants tkt invs
+    has_treesync_invariants tkt
   )
   (ensures (
     let (_, tr_out) = welcome p as_session gmgr_session kpmgr_session my_key_package group_id l t tr in
@@ -264,7 +264,7 @@ let add #tkt p as_session gmgr_session group_id ln =
   return (Some new_leaf_index)
 
 val add_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   p:principal -> as_session:state_id -> gmgr_session:state_id ->
   group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt ->
@@ -273,7 +273,7 @@ val add_proof:
   (requires
     is_well_formed _ (is_publishable tr) ln /\
     trace_invariant tr /\
-    has_treesync_invariants tkt invs
+    has_treesync_invariants tkt
   )
   (ensures (
     let (_, tr_out) = add p as_session gmgr_session group_id ln tr in
@@ -324,7 +324,7 @@ let update #tkt p as_session gmgr_session group_id ln li =
   return (Some ())
 
 val update_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   p:principal -> as_session:state_id -> gmgr_session:state_id ->
   group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> li:nat ->
@@ -333,7 +333,7 @@ val update_proof:
   (requires
     is_well_formed _ (is_publishable tr) ln /\
     trace_invariant tr /\
-    has_treesync_invariants tkt invs
+    has_treesync_invariants tkt
   )
   (ensures (
     let (_, tr_out) = update p as_session gmgr_session group_id ln li tr in
@@ -381,7 +381,7 @@ let remove #tkt p as_session gmgr_session group_id li =
   return (Some ())
 
 val remove_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   p:principal -> as_session:state_id -> gmgr_session:state_id ->
   group_id:mls_bytes dy_bytes -> li:nat ->
@@ -389,7 +389,7 @@ val remove_proof:
   Lemma
   (requires
     trace_invariant tr /\
-    has_treesync_invariants tkt invs
+    has_treesync_invariants tkt
   )
   (ensures (
     let (_, tr_out) = remove #tkt p as_session gmgr_session group_id li tr in
@@ -434,7 +434,7 @@ let commit #tkt #l #li p as_session gmgr_session group_id path =
 
 #push-options "--z3rlimit 50"
 val commit_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 ->
   p:principal -> as_session:state_id -> gmgr_session:state_id ->
   group_id:mls_bytes dy_bytes -> path:pathsync dy_bytes tkt l 0 li ->
@@ -443,7 +443,7 @@ val commit_proof:
   (requires
     is_well_formed _ (is_publishable tr) path /\
     trace_invariant tr /\
-    has_treesync_invariants tkt invs
+    has_treesync_invariants tkt
   )
   (ensures (
     let (_, tr_out) = commit p as_session gmgr_session group_id path tr in
@@ -503,13 +503,13 @@ let create_signature_keypair p =
   return (Some (private_si, (verification_key <: signature_public_key_nt dy_bytes)))
 
 val create_signature_keypair_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   p:principal ->
   tr:trace ->
   Lemma
   (requires
     trace_invariant tr /\
-    has_treesync_private_state_invariant invs
+    has_treesync_private_state_invariant
   )
   (ensures (
     let (opt_res, tr_out) = create_signature_keypair p tr in
@@ -564,7 +564,7 @@ let authenticate_path #tkt #l p gmgr_session group_id tree path =
 
 #push-options "--z3rlimit 25"
 val authenticate_path_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 ->
   p:principal -> gmgr_session:state_id ->
   group_id:mls_bytes dy_bytes -> tree:treesync dy_bytes tkt l 0 -> path:external_pathsync dy_bytes tkt l 0 li ->
@@ -574,7 +574,7 @@ val authenticate_path_proof:
     external_path_has_event p tr tree path group_id /\
     is_well_formed _ (is_publishable tr) path /\
     trace_invariant tr /\
-    has_treesync_invariants tkt invs
+    has_treesync_invariants tkt
   )
   (ensures (
     let (opt_auth_path, tr_out) = authenticate_path p gmgr_session group_id tree path tr in
@@ -635,7 +635,7 @@ let authenticate_leaf_node_data_from_key_package #tkt p si_private ln_data =
   extract_result (sign_leaf_node_data_key_package #dy_bytes #crypto_dy_bytes ln_data private_st.signature_key signature_nonce)
 
 val authenticate_leaf_node_data_from_key_package_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   p:principal ->
   si_private:state_id ->
@@ -646,7 +646,7 @@ val authenticate_leaf_node_data_from_key_package_proof:
     is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_publishable tr) ln_data /\
     leaf_node_has_event p tr ({data = ln_data; group_id = (); leaf_index = ();}) /\
     trace_invariant tr /\
-    has_treesync_invariants tkt invs
+    has_treesync_invariants tkt
   )
   (ensures (
     let (opt_ln, tr_out) = authenticate_leaf_node_data_from_key_package p si_private ln_data tr in
@@ -689,7 +689,7 @@ let authenticate_leaf_node_data_from_update #tkt p si_private ln_data group_id l
   extract_result (sign_leaf_node_data_update #dy_bytes #crypto_dy_bytes ln_data group_id leaf_index private_st.signature_key signature_nonce)
 
 val authenticate_leaf_node_data_from_update_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   p:principal ->
   si_private:state_id ->
@@ -702,7 +702,7 @@ val authenticate_leaf_node_data_from_update_proof:
     leaf_node_has_event p tr ({data = ln_data; group_id; leaf_index;}) /\
     tree_has_event p tr group_id (|0, leaf_index, TLeaf (Some ({data = ln_data; signature = empty #dy_bytes;} <: leaf_node_nt dy_bytes tkt))|) /\
     trace_invariant tr /\
-    has_treesync_invariants tkt invs
+    has_treesync_invariants tkt
   )
   (ensures (
     let (opt_ln, tr_out) = authenticate_leaf_node_data_from_update p si_private ln_data group_id leaf_index tr in
@@ -766,7 +766,7 @@ let trigger_tree_list_event_lemma #tkt p tr group_id h t =
 
 #push-options "--ifuel 1 --fuel 1 --z3rlimit 10"
 val trigger_tree_list_event_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   group_has_event_pred: event_predicate (group_has_tree_event dy_bytes tkt) ->
   p:principal ->
@@ -776,7 +776,7 @@ val trigger_tree_list_event_proof:
   (requires
     (forall t tr_extended. List.Tot.memP t tl /\ tr <$ tr_extended ==> group_has_event_pred tr_extended p (mk_group_has_tree_event group_id t)) /\
     trace_invariant tr /\
-    has_event_pred invs group_has_event_pred
+    has_event_pred group_has_event_pred
   )
   (ensures (
     let ((), tr_out) = trigger_tree_list_event p group_id tl tr in
@@ -810,7 +810,7 @@ let trigger_leaf_node_event #tkt p ln_tbs =
   trigger_event p ln_tbs
 
 val trigger_leaf_node_event_proof:
-  {|invs:protocol_invariants|} ->
+  {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   leaf_node_has_event_pred: event_predicate (leaf_node_tbs_nt dy_bytes tkt) ->
   p:principal ->
@@ -820,7 +820,7 @@ val trigger_leaf_node_event_proof:
   (requires
     leaf_node_has_event_pred tr p ln_tbs /\
     trace_invariant tr /\
-    has_event_pred invs leaf_node_has_event_pred
+    has_event_pred leaf_node_has_event_pred
   )
   (ensures (
     let ((), tr_out) = trigger_leaf_node_event p ln_tbs tr in
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
index 5de4842..c5c4022 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
@@ -52,9 +52,9 @@ let as_cache_pred #ci = {
   );
 }
 
-val has_as_cache_invariant: protocol_invariants -> prop
-let has_as_cache_invariant invs =
-  has_map_session_invariant invs as_cache_pred
+val has_as_cache_invariant: {|protocol_invariants|} -> prop
+let has_as_cache_invariant #invs =
+  has_map_session_invariant as_cache_pred
 
 val as_cache_tag_and_invariant: {|crypto_invariants|} -> string & local_bytes_state_predicate
 let as_cache_tag_and_invariant #ci = (as_cache_types.tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant as_cache_pred))
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
index 78ab9d4..930165d 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
@@ -26,18 +26,18 @@ let all_signwithlabel_preds tkt = [
   leaf_node_tbs_tag_and_invariant tkt;
 ]
 
-val mls_sign_pred: treekem_types dy_bytes -> sign_crypto_predicate treesync_crypto_usages
+val mls_sign_pred: treekem_types dy_bytes -> sign_crypto_predicate
 let mls_sign_pred tkt =
   mk_mls_sign_pred (all_signwithlabel_preds tkt)
 
-val all_sign_preds: treekem_types dy_bytes -> list (string & sign_crypto_predicate treesync_crypto_usages)
+val all_sign_preds: treekem_types dy_bytes -> list (string & sign_crypto_predicate)
 let all_sign_preds tkt = [
   ("MLS.LeafSignKey", mls_sign_pred tkt)
 ]
 
-val treesync_crypto_predicates: treekem_types dy_bytes -> crypto_predicates treesync_crypto_usages
+val treesync_crypto_predicates: treekem_types dy_bytes -> crypto_predicates
 let treesync_crypto_predicates tkt = {
-  default_crypto_predicates treesync_crypto_usages with
+  default_crypto_predicates with
   sign_pred = mk_sign_predicate (all_sign_preds tkt);
 }
 
@@ -55,14 +55,13 @@ let all_state_predicates tkt = [
   treesync_private_state_tag_and_invariant;
 ]
 
-val treesync_trace_invariants: tkt:treekem_types dy_bytes -> trace_invariants (treesync_crypto_invariants tkt)
+val treesync_trace_invariants: tkt:treekem_types dy_bytes -> trace_invariants
 let treesync_trace_invariants tkt = {
-  state_pred = mk_state_pred (treesync_crypto_invariants tkt) (all_state_predicates tkt);
+  state_pred = mk_state_pred (all_state_predicates tkt);
   event_pred = mk_event_pred [];
 }
 
-val treesync_protocol_invariants: treekem_types dy_bytes -> protocol_invariants
-let treesync_protocol_invariants tkt = {
+instance treesync_protocol_invariants (tkt:treekem_types dy_bytes): protocol_invariants = {
   crypto_invs = treesync_crypto_invariants tkt;
   trace_invs = treesync_trace_invariants tkt;
 }
@@ -78,22 +77,22 @@ let all_signwithlabel_preds_has_all_signwithlabel_preds tkt =
 #pop-options
 
 #push-options "--ifuel 1 --fuel 1"
-val all_sign_preds_has_all_sign_preds: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP (has_sign_predicate (treesync_crypto_invariants tkt)) (all_sign_preds tkt)))
+val all_sign_preds_has_all_sign_preds: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP has_sign_predicate (all_sign_preds tkt)))
 let all_sign_preds_has_all_sign_preds tkt =
   assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_sign_preds tkt)));
-  mk_sign_predicate_correct (treesync_crypto_invariants tkt) (all_sign_preds tkt);
-  norm_spec [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP (has_sign_predicate (treesync_crypto_invariants tkt)) (all_sign_preds tkt))
+  mk_sign_predicate_correct (all_sign_preds tkt);
+  norm_spec [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP has_sign_predicate (all_sign_preds tkt))
 #pop-options
 
-val all_state_predicates_has_all_state_predicates: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate (treesync_protocol_invariants tkt)) (all_state_predicates tkt)))
+val all_state_predicates_has_all_state_predicates: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP has_local_bytes_state_predicate (all_state_predicates tkt)))
 let all_state_predicates_has_all_state_predicates tkt =
   assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_state_predicates tkt)));
-  mk_state_pred_correct (treesync_protocol_invariants tkt) (all_state_predicates tkt);
-  norm_spec [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate (treesync_protocol_invariants tkt)) (all_state_predicates tkt))
+  mk_state_pred_correct (all_state_predicates tkt);
+  norm_spec [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP has_local_bytes_state_predicate (all_state_predicates tkt))
 
 val treesync_protocol_invariants_has_has_treesync_invariants: tkt:treekem_types dy_bytes -> Lemma
-  (has_treesync_invariants tkt (treesync_protocol_invariants tkt))
-  [SMTPat (has_treesync_invariants tkt (treesync_protocol_invariants tkt))]
+  (has_treesync_invariants tkt)
+  [SMTPat (has_treesync_invariants tkt)]
 let treesync_protocol_invariants_has_has_treesync_invariants tkt =
   all_signwithlabel_preds_has_all_signwithlabel_preds tkt;
   all_sign_preds_has_all_sign_preds tkt;
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
index 5c5d86d..0e0b2e6 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
@@ -174,9 +174,9 @@ val leaf_node_tbs_tag_and_invariant: {|crypto_usages|} -> treekem_types dy_bytes
 let leaf_node_tbs_tag_and_invariant #cu tkt = (leaf_node_label, leaf_node_sign_pred tkt)
 
 val has_leaf_node_tbs_invariant:
-  treekem_types dy_bytes -> crypto_invariants ->
+  treekem_types dy_bytes -> {|crypto_invariants|} ->
   prop
-let has_leaf_node_tbs_invariant tkt ci =
+let has_leaf_node_tbs_invariant tkt #ci =
   has_mls_signwithlabel_pred (leaf_node_tbs_tag_and_invariant tkt)
 
 (*** Proof of verification, for a tree ***)
@@ -305,14 +305,14 @@ let rec is_well_formed_leaf_at #bytes #bl #tkt #l #i pre t li =
 /// we conclude.
 #push-options "--z3rlimit 100"
 val parent_hash_implies_event:
-  {|ci:crypto_invariants|} ->
+  {|crypto_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   #l:nat -> #i:tree_index l ->
   tr:trace ->
   group_id:mls_bytes dy_bytes -> t:treesync dy_bytes tkt l i -> ast:as_tokens dy_bytes (dy_asp tr).token_t l i ->
   Lemma
   (requires
-    has_leaf_node_tbs_invariant tkt ci /\
+    has_leaf_node_tbs_invariant tkt /\
     unmerged_leaves_ok t /\
     parent_hash_invariant t /\
     valid_leaves_invariant group_id t /\
@@ -440,13 +440,13 @@ let rec all_credentials_ok_subtree #bytes #cb #tkt #asp #lp #ld #ip #id d p ast_
 /// - or the principal at the leaf is corrupt.
 /// This theorem is mostly a wrapper around `parent_hash_implies_event`.
 val state_implies_event:
-  {|ci:crypto_invariants|} ->
+  {|crypto_invariants|} ->
   #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> #l:nat -> #i:tree_index l ->
   tr:trace ->
   st:treesync_state dy_bytes tkt dy_as_token group_id -> t:treesync dy_bytes tkt l i -> ast:as_tokens dy_bytes (dy_asp tr).token_t l i ->
   Lemma
   (requires
-    has_leaf_node_tbs_invariant tkt ci /\
+    has_leaf_node_tbs_invariant tkt /\
     node_has_parent_hash t /\
     is_well_formed _ (bytes_invariant tr) (st.tree <: treesync _ _ _ _) /\
     bytes_invariant tr group_id /\
@@ -642,7 +642,7 @@ let external_path_has_event #tkt #l #li prin tr t p group_id =
 /// With label= SecrecyLabels.private_label, we get a version with `is_valid`.
 #push-options "--z3rlimit 100"
 val is_msg_external_path_to_path:
-  {|ci:crypto_invariants|} ->
+  {|crypto_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   #l:nat -> #li:leaf_index l 0 ->
   prin:principal -> label:label -> tr:trace ->
@@ -662,7 +662,7 @@ val is_msg_external_path_to_path:
     bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
     get_label sk == principal_label prin /\
     get_label nonce == principal_label prin /\
-    has_leaf_node_tbs_invariant tkt ci
+    has_leaf_node_tbs_invariant tkt
   )
   (ensures is_well_formed _ (is_knowable_by label tr) (Success?.v (external_path_to_path t p group_id sk nonce)))
 let is_msg_external_path_to_path #ci #tkt #l #li prin label tr t p group_id sk nonce =
@@ -703,7 +703,7 @@ let is_msg_external_path_to_path #ci #tkt #l #li prin label tr t p group_id sk n
 
 #push-options "--z3rlimit 25"
 val is_msg_sign_leaf_node_data_key_package:
-  {|ci:crypto_invariants|} ->
+  {|crypto_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   prin:principal -> label:label -> tr:trace ->
   ln_data:leaf_node_data_nt dy_bytes tkt ->
@@ -718,7 +718,7 @@ val is_msg_sign_leaf_node_data_key_package:
     bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
     get_label sk == principal_label prin /\
     get_label nonce == principal_label prin /\
-    has_leaf_node_tbs_invariant tkt ci
+    has_leaf_node_tbs_invariant tkt
   )
   (ensures is_well_formed _ (is_knowable_by label tr) (Success?.v (sign_leaf_node_data_key_package ln_data sk nonce)))
 let is_msg_sign_leaf_node_data_key_package #ci #tkt prin label tr ln_data sk nonce =
@@ -731,7 +731,7 @@ let is_msg_sign_leaf_node_data_key_package #ci #tkt prin label tr ln_data sk non
 
 #push-options "--z3rlimit 25"
 val is_msg_sign_leaf_node_data_update:
-  {|ci:crypto_invariants|} ->
+  {|crypto_invariants|} ->
   #tkt:treekem_types dy_bytes ->
   prin:principal -> label:label -> tr:trace ->
   ln_data:leaf_node_data_nt dy_bytes tkt -> group_id:mls_bytes dy_bytes -> leaf_index:nat_lbytes 4 ->
@@ -748,7 +748,7 @@ val is_msg_sign_leaf_node_data_update:
     bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
     get_label sk == principal_label prin /\
     get_label nonce == principal_label prin /\
-    has_leaf_node_tbs_invariant tkt ci
+    has_leaf_node_tbs_invariant tkt
   )
   (ensures is_well_formed _ (is_knowable_by label tr) (Success?.v (sign_leaf_node_data_update ln_data group_id leaf_index sk nonce)))
 let is_msg_sign_leaf_node_data_update #ci #tkt prin label tr ln_data group_id leaf_index sk nonce =