diff --git a/flake.lock b/flake.lock
index 21a440f..9ec5358 100644
--- a/flake.lock
+++ b/flake.lock
@@ -36,11 +36,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1728999480,
-        "narHash": "sha256-hdopgcd4utijr5j2vmXY164h/6cnf24QtK1RMAZjgVM=",
+        "lastModified": 1729090944,
+        "narHash": "sha256-v61k1JYcQUNojjJZFD3IpjZKrEvGVohOPiWSsYMK+Dk=",
         "owner": "REPROSEC",
         "repo": "dolev-yao-star-extrinsic",
-        "rev": "92b62fb8c93cbed961e165c9da32c2d1fe34a373",
+        "rev": "57903cfeb6224dd788b1a72ea9fba72706a0eb76",
         "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 6687f76..5fc399d 100644
--- a/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
+++ b/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
@@ -15,18 +15,17 @@ open MLS.Result
 
 noeq
 type signwithlabel_crypto_pred {|crypto_usages|} = {
-  pred: trace -> vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes -> prop;
+  pred: trace -> sk_usg:usage{SigKey? sk_usg} -> msg:bytes -> prop;
   pred_later:
     tr1:trace -> tr2:trace ->
-    vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes ->
+    sk_usg:usage{SigKey? sk_usg} -> msg:bytes ->
     Lemma
     (requires
-      pred tr1 vk msg /\
-      bytes_well_formed tr1 vk /\
+      pred tr1 sk_usg msg /\
       bytes_well_formed tr1 msg /\
       tr1 <$ tr2
     )
-    (ensures pred tr2 vk msg)
+    (ensures pred tr2 sk_usg msg)
   ;
 }
 
@@ -41,8 +40,8 @@ let split_signwithlabel_crypto_pred_params {|crypto_usages|}: split_function_par
     FStar.Classical.move_requires_2 get_mls_label_inj tag_set_1 tag_set_2
   );
 
-  tagged_data_t = (trace & (vk:bytes{SigKey? (get_signkey_usage vk)}) & bytes);
-  raw_data_t = (trace & (vk:bytes{SigKey? (get_signkey_usage vk)}) & bytes);
+  tagged_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes);
+  raw_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes);
   output_t = prop;
 
   decode_tagged_data = (fun (tr, vk, data) -> (
@@ -52,7 +51,7 @@ let split_signwithlabel_crypto_pred_params {|crypto_usages|}: split_function_par
   ));
 
   local_fun_t = mk_dependent_type signwithlabel_crypto_pred;
-  global_fun_t = trace -> vk:bytes{SigKey? (get_signkey_usage vk)} -> bytes -> prop;
+  global_fun_t = trace -> sk_usg:usage{SigKey? sk_usg} -> bytes -> prop;
 
   default_global_fun = (fun tr vk content -> False);
 
@@ -102,7 +101,7 @@ let intro_has_signwithlabel_pred #cusgs sign_pred tag local_pred =
 val mk_global_mls_sign_pred:
   {|crypto_usages|} ->
   list (valid_label & signwithlabel_crypto_pred) ->
-  trace -> vk:bytes{SigKey? (get_signkey_usage vk)} -> bytes ->
+  trace -> sk_usg:usage{SigKey? sk_usg} -> bytes ->
   prop
 let mk_global_mls_sign_pred tagged_local_preds vk msg =
   mk_global_fun split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) vk msg
@@ -112,22 +111,21 @@ val mk_global_mls_sign_pred_later:
   {|crypto_usages|} ->
   tagged_local_preds:list (valid_label & signwithlabel_crypto_pred) ->
   tr1:trace -> tr2:trace ->
-  vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes ->
+  sk_usg:usage{SigKey? sk_usg} -> msg:bytes ->
   Lemma
   (requires
-    mk_global_mls_sign_pred tagged_local_preds tr1 vk msg /\
-    bytes_well_formed tr1 vk /\
+    mk_global_mls_sign_pred tagged_local_preds tr1 sk_usg msg /\
     bytes_well_formed tr1 msg /\
     tr1 <$ tr2
   )
-  (ensures mk_global_mls_sign_pred tagged_local_preds tr2 vk msg)
-let mk_global_mls_sign_pred_later tagged_local_preds tr1 tr2 vk msg =
-  mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr1, vk, msg);
-  mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr2, vk, msg);
+  (ensures mk_global_mls_sign_pred tagged_local_preds tr2 sk_usg msg)
+let mk_global_mls_sign_pred_later tagged_local_preds tr1 tr2 sk_usg msg =
+  mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr1, sk_usg, msg);
+  mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr2, sk_usg, msg);
   FStar.Classical.move_requires (parse_wf_lemma (sign_content_nt bytes) (bytes_well_formed tr1)) msg;
-  introduce forall tag_set lpred content. bytes_well_formed tr1 content /\ split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr1, vk, content) ==> split_signwithlabel_crypto_pred_params.apply_local_fun #tag_set lpred (tr2, vk, content) with (
+  introduce forall tag_set lpred content. bytes_well_formed tr1 content /\ split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr1, sk_usg, content) ==> split_signwithlabel_crypto_pred_params.apply_local_fun #tag_set lpred (tr2, sk_usg, content) with (
     introduce _ ==> _ with _. (
-      lpred.pred_later tr1 tr2 vk content
+      lpred.pred_later tr1 tr2 sk_usg content
     )
   )
 #pop-options
@@ -179,10 +177,13 @@ val bytes_invariant_sign_with_label:
     bytes_invariant tr sk /\
     bytes_invariant tr nonce /\
     bytes_invariant tr msg /\
-    get_usage sk == mk_mls_sigkey_usage prin /\
-    SigNonce? (get_usage nonce) /\
-    (get_label tr sk) `can_flow tr` (get_label tr nonce) /\
-    spred.pred tr (vk sk) msg /\
+    sk `has_usage tr` mk_mls_sigkey_usage prin /\
+    nonce `has_usage tr` SigNonce /\
+    (get_label tr sk) `can_flow tr` (get_label tr nonce) /\ (
+      spred.pred tr (mk_mls_sigkey_usage prin) msg
+      \/
+      get_label tr sk `can_flow tr` public
+    ) /\
     has_mls_signwithlabel_pred (lab, spred)
   )
   (ensures
@@ -206,13 +207,13 @@ val bytes_invariant_verify_with_label:
     bytes_invariant tr vk /\
     bytes_invariant tr content /\
     bytes_invariant tr signature /\
+    vk `has_signkey_usage tr` mk_mls_sigkey_usage prin /\
     verify_with_label vk lab content signature /\
     has_mls_signwithlabel_pred (lab, spred)
   )
   (ensures
     (
-      get_signkey_usage vk == mk_mls_sigkey_usage prin ==>
-      spred.pred tr vk content
+      spred.pred tr (mk_mls_sigkey_usage prin) content
     ) \/ (
       (get_signkey_label tr vk) `can_flow tr` public
     )
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst
index e5458c7..64df43b 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst
@@ -48,8 +48,8 @@ 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))
+val group_manager_tag_and_invariant: {|crypto_invariants|} -> dtuple2 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)|)
 
 (*** Group manager API ***)
 
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst
index 47b1ef9..7a1e2cc 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst
@@ -31,7 +31,7 @@ let key_package_manager_pred #ci tkt = {
   );
   pred_later = (fun tr1 tr2 prin state_id key_package value -> ());
   pred_knowable = (fun tr prin state_id key_package value ->
-    assert(is_well_formed _ (is_knowable_by (principal_state_label prin state_id) tr) key_package)
+    assert(is_well_formed _ (is_knowable_by (principal_tag_state_label prin (key_package_manager_types tkt).tag state_id) tr) key_package)
   );
 }
 
@@ -39,8 +39,8 @@ val has_key_package_manager_invariant: treekem_types dy_bytes -> {|protocol_inva
 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)))
+val key_package_manager_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> dtuple2 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))|)
 
 (*** KeyPackage manager API ***)
 
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
index 6623e57..863bed3 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
@@ -64,6 +64,9 @@ type bare_treesync_state (tkt:treekem_types dy_bytes) =
 
 instance parseable_serializeable_bare_treesync_state (tkt:treekem_types dy_bytes): parseable_serializeable dy_bytes (bare_treesync_state tkt) = mk_parseable_serializeable (ps_bare_treesync_state_ tkt dy_as_token ps_dy_as_token)
 
+instance local_state_bare_treesync_state (tkt:treekem_types dy_bytes): local_state (bare_treesync_state tkt) =
+  mk_local_state_instance "MLS.TreeSync.PublicState"
+
 #push-options "--fuel 1 --ifuel 1 --z3rlimit 25"
 val treesync_public_state_pred: {|crypto_invariants|} -> tkt:treekem_types dy_bytes -> local_state_predicate (bare_treesync_state tkt)
 let treesync_public_state_pred #ci tkt = {
@@ -79,22 +82,19 @@ let treesync_public_state_pred #ci tkt = {
     wf_weaken_lemma _ (is_publishable tr1) (is_publishable tr2) st.tree
   );
   pred_knowable = (fun tr prin state_id st ->
-    let pre = is_knowable_by (principal_state_label prin state_id) tr in
+    let pre = is_knowable_by (principal_typed_state_content_label prin (local_state_bare_treesync_state tkt).tag state_id st) tr in
     wf_weaken_lemma _ (is_publishable tr) pre st.tree;
     ps_dy_as_tokens_is_well_formed pre st.tokens
   );
 }
 #pop-options
 
-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 (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))
+val treesync_public_state_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> dtuple2 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)|)
 
 (*** Traceful API for public state ***)
 
@@ -219,6 +219,9 @@ type treesync_private_state = treesync_private_state_ dy_bytes
 
 instance parseable_serializeable_treesync_private_state: parseable_serializeable dy_bytes treesync_private_state = mk_parseable_serializeable ps_treesync_private_state_
 
+instance local_state_treesync_private_state: local_state treesync_private_state =
+  mk_local_state_instance "MLS.TreeSync.PrivateState"
+
 val treesync_private_state_pred: {|crypto_invariants|} -> local_state_predicate treesync_private_state
 let treesync_private_state_pred #ci = {
   pred = (fun tr prin state_id st ->
@@ -228,15 +231,12 @@ let treesync_private_state_pred #ci = {
   pred_knowable = (fun tr prin state_id st -> ());
 }
 
-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 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)
+val treesync_private_state_tag_and_invariant: {|crypto_invariants|} -> dtuple2 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|)
 
 (*** Traceful API for private state ***)
 
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
index 9cdfde4..d6eac2f 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
@@ -159,6 +159,7 @@ let create #tkt p as_session gmgr_session group_id ln secret_session =
   add_new_group_sessions p gmgr_session { group_id } group_sessions;*?
   return (Some ())
 
+#push-options "--z3rlimit 25"
 val create_proof:
   {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
@@ -189,6 +190,7 @@ let create_proof #invs #tkt p as_session gmgr_session group_id ln secret_session
       finalize_create_valid #_ #_ #_ #(dy_asp tr) create_pend token
     )
   )
+#pop-options
 
 val welcome:
   #tkt:treekem_types dy_bytes ->
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
index 6b84d93..5c4693e 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
@@ -41,12 +41,12 @@ let as_cache_pred #ci = {
     value.time <= DY.Core.Trace.Base.length tr /\
     is_publishable (prefix tr value.time) key.verification_key /\
     get_signkey_label tr key.verification_key == principal_label value.who /\
-    get_signkey_usage key.verification_key == mk_mls_sigkey_usage value.who /\
+    key.verification_key `has_signkey_usage tr` mk_mls_sigkey_usage value.who /\
     is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_publishable (prefix tr value.time)) key.credential
   );
   pred_later = (fun tr1 tr2 prin state_id key value -> ());
   pred_knowable = (fun tr prin state_id key value ->
-    assert(is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_knowable_by (principal_state_label prin state_id) tr) key.credential)
+    assert(is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_knowable_by (principal_tag_state_label prin as_cache_types.tag state_id) tr) key.credential)
   );
 }
 
@@ -54,8 +54,8 @@ 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))
+val as_cache_tag_and_invariant: {|crypto_invariants|} -> dtuple2 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)|)
 
 (*** AS cache API ***)
 
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
index 930165d..ee96c88 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
@@ -46,7 +46,7 @@ instance treesync_crypto_invariants (tkt:treekem_types dy_bytes): crypto_invaria
   preds = treesync_crypto_predicates tkt;
 }
 
-val all_state_predicates: tkt:treekem_types dy_bytes -> list (string & local_bytes_state_predicate)
+val all_state_predicates: tkt:treekem_types dy_bytes -> list (dtuple2 string local_bytes_state_predicate)
 let all_state_predicates tkt = [
   as_cache_tag_and_invariant;
   group_manager_tag_and_invariant;
@@ -86,7 +86,7 @@ let all_sign_preds_has_all_sign_preds 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)));
+  assert_norm(List.Tot.no_repeats_p (List.Tot.map dfst (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))
 
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
index f498f56..8c2d25a 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
@@ -47,7 +47,7 @@ let dy_asp #ci tr = {
   credential_ok = (fun (vk, cred) token ->
     token.time <= (DY.Core.Trace.Base.length tr) /\
     bytes_invariant (prefix tr token.time) vk /\
-    get_signkey_usage vk == mk_mls_sigkey_usage token.who /\
+    vk `has_signkey_usage tr` mk_mls_sigkey_usage token.who /\
     get_signkey_label tr vk == principal_label token.who
   );
   valid_successor = (fun (vk_old, cred_old) (vk_new, cred_new) ->
@@ -137,12 +137,12 @@ val leaf_node_sign_pred:
   {|crypto_usages|} -> treekem_types dy_bytes ->
   signwithlabel_crypto_pred
 let leaf_node_sign_pred #cu tkt = {
-  pred = (fun tr vk ln_tbs_bytes ->
+  pred = (fun tr sk_usg ln_tbs_bytes ->
     match (parse (leaf_node_tbs_nt dy_bytes tkt) ln_tbs_bytes) with
     | None -> False
     | Some ln_tbs -> (
       exists prin.
-        get_signkey_usage vk == mk_mls_sigkey_usage prin /\
+        sk_usg == mk_mls_sigkey_usage prin /\
         leaf_node_has_event prin tr ln_tbs /\ (
         match ln_tbs.data.source with
         | LNS_commit -> (
@@ -351,24 +351,23 @@ let parent_hash_implies_event #ci #tkt #l #i tr group_id t ast =
   serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (bytes_invariant tr) ln_tbs;
   bytes_invariant_verify_with_label (leaf_node_sign_pred  tkt) tr authentifier ln.data.signature_key "LeafNodeTBS" ln_tbs_bytes ln.signature;
 
-  introduce ((leaf_node_sign_pred tkt).pred tr ln.data.signature_key ln_tbs_bytes) ==> tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|)
+  introduce ((leaf_node_sign_pred tkt).pred tr (mk_mls_sigkey_usage authentifier) ln_tbs_bytes) ==> tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|)
   with _. (
     (
       parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) ln_tbs;
 
-      eliminate exists (prin:principal) (leaf_tl: tree_list dy_bytes tkt).
-        get_signkey_usage ln.data.signature_key == mk_mls_sigkey_usage prin /\
+      eliminate exists (leaf_tl: tree_list dy_bytes tkt).
         tree_list_starts_with_tbs leaf_tl ln_tbs_bytes /\
         tree_list_is_parent_hash_linkedP leaf_tl /\
         tree_list_ends_at_root leaf_tl /\
         tree_list_is_canonicalized authentifier_li leaf_tl /\
-        tree_list_has_event prin tr ln_tbs.group_id leaf_tl
+        tree_list_has_event authentifier tr ln_tbs.group_id leaf_tl
       returns tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|)
       with _. (
         let (b1, b2) = parent_hash_guarantee_theorem my_tl leaf_tl ln_tbs_bytes in
         FStar.Classical.move_requires_2 hash_injective b1 b2;
         last_tree_equivalent my_tl leaf_tl leaf_i;
-        for_allP_eq (tree_has_event prin tr group_id) leaf_tl;
+        for_allP_eq (tree_has_event authentifier tr group_id) leaf_tl;
         let (|_, _, original_t|) = List.Tot.index leaf_tl (List.Tot.length my_tl - 1) in
         List.Tot.lemma_index_memP leaf_tl (List.Tot.length my_tl - 1);
         for_allP_eq (tree_is_canonicalized authentifier_li) leaf_tl;
@@ -658,8 +657,8 @@ val is_msg_external_path_to_path:
     is_well_formed _ (is_knowable_by label tr) t /\
     is_well_formed _ (is_knowable_by label tr) p /\
     is_knowable_by label tr group_id /\
-    bytes_invariant tr sk /\ get_usage sk == mk_mls_sigkey_usage prin /\
-    bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
+    bytes_invariant tr sk /\ sk `has_usage tr` mk_mls_sigkey_usage prin /\
+    bytes_invariant tr nonce /\ nonce `has_usage tr` SigNonce /\
     get_label tr sk == principal_label prin /\
     get_label tr nonce == principal_label prin /\
     has_leaf_node_tbs_invariant tkt
@@ -714,8 +713,8 @@ val is_msg_sign_leaf_node_data_key_package:
     Success? (sign_leaf_node_data_key_package ln_data sk nonce) /\
     leaf_node_has_event prin tr ({data = ln_data; group_id = (); leaf_index = ();}) /\
     is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_knowable_by label tr) ln_data /\
-    bytes_invariant tr sk /\ get_usage sk == mk_mls_sigkey_usage prin /\
-    bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
+    bytes_invariant tr sk /\ sk `has_usage tr` mk_mls_sigkey_usage prin /\
+    bytes_invariant tr nonce /\ nonce `has_usage tr` SigNonce /\
     get_label tr sk == principal_label prin /\
     get_label tr nonce == principal_label prin /\
     has_leaf_node_tbs_invariant tkt
@@ -744,8 +743,8 @@ val is_msg_sign_leaf_node_data_update:
     tree_has_event prin tr group_id (|0, (leaf_index <: nat), TLeaf (Some ({data = ln_data; signature = empty #dy_bytes;} <: leaf_node_nt dy_bytes tkt))|) /\
     is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_knowable_by label tr) ln_data /\
     is_knowable_by label tr group_id /\
-    bytes_invariant tr sk /\ get_usage sk == mk_mls_sigkey_usage prin /\
-    bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
+    bytes_invariant tr sk /\ sk `has_usage tr` mk_mls_sigkey_usage prin /\
+    bytes_invariant tr nonce /\ nonce `has_usage tr` SigNonce /\
     get_label tr sk == principal_label prin /\
     get_label tr nonce == principal_label prin /\
     has_leaf_node_tbs_invariant tkt