diff --git a/examples/Online_with_secrecy/DY.OnlineS.Invariants.Proofs.fst b/examples/Online_with_secrecy/DY.OnlineS.Invariants.Proofs.fst
index 7dc7ae5..f152509 100644
--- a/examples/Online_with_secrecy/DY.OnlineS.Invariants.Proofs.fst
+++ b/examples/Online_with_secrecy/DY.OnlineS.Invariants.Proofs.fst
@@ -44,50 +44,41 @@ val send_ping_invariant:
    so we have to unfold the monadic lets and sequences.)
 *)
 let send_ping_invariant alice bob keys_sid  tr =
-  (* The first action is generating the nonce n_a.
-  
-     Note that we can't use let* here since we are not in the traceful monad.
-     Thus, we have to pass the trace `tr` explicitly as last argument.
-     And we get back the new trace `tr_rand`.
-  *)
-  let (n_a, tr_rand) = gen_rand_labeled (nonce_label alice bob) tr in
-  (* That the trace invariant holds after this action,
-     can be shown automatically.
+   match send_ping alice bob keys_sid tr with
+   | (None, _) -> ()
+   | (Some (state_id, msg_id), tr_out) -> (
+      (* The first action is generating the nonce n_a.
+      
+         Note that we can't use let* here since we are not in the traceful monad.
+         Thus, we have to pass the trace `tr` explicitly as last argument.
+         And we get back the new trace `tr_rand`.
+      *)
+      let (n_a, tr_rand) = gen_rand_labeled (nonce_label alice bob) tr in
+      (* That the trace invariant holds after this action,
+         can be shown automatically.
 
-     There is a corresponding lemma in `DY.Core.Trace.Manipulation`:
-     `mk_rand_trace_invariant`.
-     It comes with an SMT Pattern an hence is applied automatically.
-  *)
-  assert(trace_invariant tr_rand);
+         There is a corresponding lemma in `DY.Core.Trace.Manipulation`:
+         `mk_rand_trace_invariant`.
+         It comes with an SMT Pattern an hence is applied automatically.
+      *)
+      assert(trace_invariant tr_rand);
 
-  // Defining the abstract message does not change the trace,
-  // so we don't have to show anything.
-  let ping = Ping {alice; n_a} in 
+      // Defining the abstract message does not change the trace,
+      // so we don't have to show anything.
+      let ping = Ping {alice; n_a} in 
 
-  (* The call of `pk_enc_for` in the traceful + option monad 
-     has to be unfolded:
-     * We pass the current trace `tr_rand` as las argument
-     * We need to make a case distinction on the resulting option
-       and show trace_invariant in each case separately
-  *)
-  match pk_enc_for alice bob keys_sid key_tag ping tr_rand with
-  | (None, _) -> ( 
-      (* If encryption fails, the trace is not changed,
-         and hence the resulting trace after send_ping is tr_rand.
-         Since we already showed trace_invariant for tr_rand,
-         we don't have to show anything else in this case.
-
-        If you want to check this,
-        you can uncomment the next lines
+      (* The call of `pk_enc_for` in the traceful + option monad 
+         has to be unfolded:
+         As before, we pass the current trace `tr_rand` as last argument
+
+         Since the overall `send_ping` function is successful,
+         i.e., returns a Some,
+         we know that this step must also return a Some.
+         We can thus, immediately pattern match the result of
+         `pke_enc_for` to a Some and obtain a new trace `tr_enc`.
       *)
-      // let (_ , tr_out) = send_ping alice bob keys_sid tr in 
-      // assert(tr_out == tr_rand);
-      // assert(trace_invariant tr_out);
-      ()
-    )
-  | (Some ping_encrypted, tr_enc) -> (
-      (* If encryption succeeds, we get a new trace `tr_enc`.
-         With the lemma `pk_enc_for_invariant` in `DY.Simplified`,
+      let (Some ping_encrypted, tr_enc) = pk_enc_for alice bob keys_sid key_tag ping tr_rand in
+      (* With the lemma `pk_enc_for_invariant` in `DY.Simplified`,
          we have that trace_invariant holds for tr_enc.
 
          Observe, that this lemma can be shown automatically.
@@ -196,8 +187,14 @@ let send_ping_invariant alice bob keys_sid  tr =
          Since that lemma comes with an SMT pattern,
          it is applied automatically.
       *)
-      assert(trace_invariant tr_sess)
-  )
+      assert(trace_invariant tr_sess);
+
+      (* Finally, we observe that the current trace `tr_sess`
+         is exactly the trace `tr_out` after the whole `send_ping` step.
+      *)
+      assert(tr_out == tr_sess)
+      (* Thus, the trace invariant must hold for `tr_out` concluding the proof. *)
+   )
 
 (* The above proof was very detailed.
    In fact, most of the proof is done automatically by F*
@@ -279,104 +276,104 @@ val receive_ping_and_send_ack_invariant:
     trace_invariant tr_out
   ))
 let receive_ping_and_send_ack_invariant bob bob_keys_sid msg_ts tr =
+  match receive_ping_and_send_ack bob bob_keys_sid msg_ts tr with
+  | (None, _ ) -> ()
+  | (Some (sid, ack_ts), tr_out) ->
   (* As for the first protocol step,
      we need to show that every traceful action 
      maintains the trace invariant.
   *)
-  match recv_msg msg_ts tr with // unfold the traceful + option let
-  | (None, _ ) -> () // in this case the trace is not changed and hence the trace invariant is trivially satisfied
-  | (Some msg, _) -> (
-      (* From the lemma `recv_msg_same_trace` in `DY.Core.Trace.Manipulation` 
-         we have that the receive function does not change the trace
-         and hence the trace invariant is still satisfied. *)
-      match decode_ping bob bob_keys_sid.private_keys msg tr with // unfold the next monadic let
-      | (None, _) -> () // Again, if decoding fails, the trace is not changed and hence nothing left to show
-      | (Some png, _) -> (
-          (* Decoding the ping message does not change the trace.
-             So we are still working on the input trace tr,
-             for which we know the trace invariant.
-
-             That decoding doesn't change the trace,
-             is shown automatically 
-             with corresponding SMT patterns for the individual steps of the function.
-             I.e., try uncommenting the following lemma:
-           *) 
-             // let decode_ping_same_trace
-             //    (p:principal) (keys_sid:state_id) (msg:bytes) (tr:trace) :
-             //    Lemma (
-             //       let (_, tr_out) = decode_ping p keys_sid msg tr in
-             //       tr_out == tr )
-             //    = () in
-          
-          let n_a = png.n_a in
-          let alice = png.alice in
-          
-          let ack = Ack {n_a} in
-          
-          match pk_enc_for bob alice bob_keys_sid.pki key_tag ack tr with
-          | (None, _) -> ()
-          | (Some ack_encrypted, tr_ack) ->(
-                (* As before, encryption maintains the trace invariant 
-                   (see `pk_enc_for_invariant` in `DY.simplified`) *)
-                assert(trace_invariant tr_ack);
-
-                let (ack_ts, tr_msg) = send_msg ack_encrypted tr_ack in
-                (* The same as in the first protocol step:
-                   we want to use the lemma `send_msg_invariant` from `DY.Core.Trace.Manipulation`
-                   to show that sending the encrypted ack maintains the invariant.
-
-                   For this, we need to show that the encrypted ack is publishable.
-                   Again, we want to apply the lemma `pk_enc_for_is_publishable` from `DY.Simplified`.
-                   So we have to show all of the pre-conditions of this lemma.
-                *)
-                  (* `trace_invariant tr` and `has_pki_invariant` are satisfied *)
-                  (* For `bytes_invariant` of the serialized ack,
-                     we need a helper lemma.
-
-                     TODO ....
-                  *)
-                  decode_ping_proof tr bob bob_keys_sid.private_keys msg;
-                  serialize_wf_lemma message_t (bytes_invariant tr) (ack);
-                  assert(bytes_invariant tr (serialize message_t ack));
-                  
-                  (* From this helper lemma, we also get
-                     that the nonce is readable by alice and bob.
-
-                     We use this fact together with a comparse lemma,
-                     to show the next two requirements:
-                     the serialized ack is readable by alice and bob 
-                     (again ignoring the `long_term_key_label`) *)
-                  assert(is_knowable_by (nonce_label alice bob) tr n_a);
-                  serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr) ack;
-
-                  (* The final requirement is trivially satisfied, 
-                     since the pkenc_pred for an Ack is just True
-
-                     You can check:
-                     assert(pkenc_pred.pred tr (long_term_key_type_to_usage (LongTermPkEncKey key_tag) alice) (serialize message_t ack));
-                  *)
-                (* Thus, we can call `pk_enc_for_is_publishable`
-                   to get the missing pre-condition for `send_msg_invariant`.*)
-                pk_enc_for_is_publishable tr bob alice bob_keys_sid.pki key_tag ack;
-                assert(trace_invariant tr_msg);
-
-                (* As in the first protocol step,
-                   starting a new session maintains the trace invariant,
-                   if the new state satisfies the state predicate.
-
-                   For the new SentAck state, this means that
-                   the stored nonce
-                   must be readble by
-                   the storing principal (here bob).
-
-                   We get this property from our helper lemma `decode_ping_proof`.
-                *)
-                let st = (SentAck {alice = png.alice; n_a = png.n_a}) in
-                let (sess_id, tr_sess) = start_new_session bob st tr_msg in
-                assert(trace_invariant tr_sess)
-           )
-      )
-  )
+  let (Some msg, _) = recv_msg msg_ts tr in // unfold the traceful + option let
+  (* From the lemma `recv_msg_same_trace` in `DY.Core.Trace.Manipulation` 
+     we have that the receive function does not change the trace
+     and hence the trace invariant is still satisfied. *)
+  let (Some png, _) = decode_ping bob bob_keys_sid.private_keys msg tr in // unfold the next monadic let
+  (* Decoding the ping message does not change the trace.
+    So we are still working on the input trace tr,
+    for which we know the trace invariant.
+
+    That decoding doesn't change the trace,
+    is shown automatically 
+    with corresponding SMT patterns for the individual steps of the function.
+    I.e., try uncommenting the following lemma:
+  *) 
+    // let decode_ping_same_trace
+    //    (p:principal) (keys_sid:state_id) (msg:bytes) (tr:trace) :
+    //    Lemma (
+    //       let (_, tr_out) = decode_ping p keys_sid msg tr in
+    //       tr_out == tr )
+    //    = () in
+
+  let n_a = png.n_a in
+  let alice = png.alice in
+
+  let ack = Ack {n_a} in
+
+  let (Some ack_encrypted, tr_ack) = pk_enc_for bob alice bob_keys_sid.pki key_tag ack tr in
+  (* As before, encryption maintains the trace invariant 
+     (see `pk_enc_for_invariant` in `DY.simplified`) *)
+  assert(trace_invariant tr_ack);
+
+  let (ack_ts, tr_msg) = send_msg ack_encrypted tr_ack in
+  (* The same as in the first protocol step:
+     we want to use the lemma `send_msg_invariant` from `DY.Core.Trace.Manipulation`
+     to show that sending the encrypted ack maintains the invariant.
+
+     For this, we need to show that the encrypted ack is publishable.
+     Again, we want to apply the lemma `pk_enc_for_is_publishable` from `DY.Simplified`.
+     So we have to show all of the pre-conditions of this lemma.
+  *)
+      (* `trace_invariant tr` and `has_pki_invariant` are satisfied *)
+      (* For `bytes_invariant` of the serialized ack,
+         we need a helper lemma.
+
+         TODO ....
+      *)
+      decode_ping_proof tr bob bob_keys_sid.private_keys msg;
+      serialize_wf_lemma message_t (bytes_invariant tr) (ack);
+      assert(bytes_invariant tr (serialize message_t ack));
+
+      (* From this helper lemma, we also get
+         that the nonce is readable by alice and bob.
+
+         We use this fact together with a comparse lemma,
+         to show the next two requirements:
+         the serialized ack is readable by alice and bob 
+         (again ignoring the `long_term_key_label`) *)
+      assert(is_knowable_by (nonce_label alice bob) tr n_a);
+      serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr) ack;
+
+      (* The final requirement is trivially satisfied, 
+         since the pkenc_pred for an Ack is just True
+
+         You can check:
+         assert(pkenc_pred.pred tr (long_term_key_type_to_usage (LongTermPkEncKey key_tag) alice) (serialize message_t ack));
+      *)
+  (* Thus, we can call `pk_enc_for_is_publishable`
+     to get the missing pre-condition for `send_msg_invariant`.*)
+  pk_enc_for_is_publishable tr bob alice bob_keys_sid.pki key_tag ack;
+  assert(trace_invariant tr_msg);
+
+  (* As in the first protocol step,
+     starting a new session maintains the trace invariant,
+     if the new state satisfies the state predicate.
+
+     For the new SentAck state, this means that
+     the stored nonce
+     must be readble by
+     the storing principal (here bob).
+
+     We get this property from our helper lemma `decode_ping_proof`.
+  *)
+  let st = (SentAck {alice = png.alice; n_a = png.n_a}) in
+  let (sess_id, tr_sess) = start_new_session bob st tr_msg in
+  assert(trace_invariant tr_sess);
+  
+  (* And again, the current trace `tr_sess` is exactly
+     the trace after the whole `receive_ping_and_send_ack` step.
+  *)
+  assert(tr_out == tr_sess)
+
 
 
 
diff --git a/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Stateful.Proof.fst b/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Stateful.Proof.fst
index ffd765b..4c1b8a3 100644
--- a/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Stateful.Proof.fst
+++ b/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Stateful.Proof.fst
@@ -155,6 +155,7 @@ val prepare_msg1_proof:
 let prepare_msg1_proof tr alice bob =
   ()
 
+#push-options "--ifuel 3"
 val send_msg1_proof:
   tr:trace ->
   global_sess_id:nsl_global_sess_ids -> alice:principal -> sess_id:state_id ->
@@ -164,18 +165,9 @@ val send_msg1_proof:
     let (opt_msg_id, tr_out) = send_msg1 global_sess_id alice sess_id tr in
     trace_invariant tr_out
   ))
-let send_msg1_proof tr global_sess_id alice sess_id =
-  match get_state alice sess_id tr with
-  | (Some (InitiatorSendingMsg1 bob n_a), tr) -> (
-      assert(state_was_set_some_id tr alice (InitiatorSendingMsg1 bob n_a));
-    match get_public_key alice global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") bob tr with
-    | (None, tr) -> ()
-    | (Some pk_b, tr) -> (
-      let (nonce, tr) = mk_rand PkNonce (long_term_key_label alice) 32 tr in
-      compute_message1_proof tr alice bob pk_b n_a nonce
-    )
-  )
-  | _ -> ()
+let send_msg1_proof tr global_sess_id alice sess_id = 
+  ()
+#pop-options
 
 val send_msg1__proof:
   tr:trace ->
@@ -187,23 +179,7 @@ val send_msg1__proof:
     trace_invariant tr_out
   ))
 let send_msg1__proof tr global_sess_id alice bob =
-  let (n_a, tr) = mk_rand NoUsage (join (principal_label alice) (principal_label bob)) 32 tr in
-  
-  let (sess_id, _) = new_session_id alice tr in
-  let st = InitiatorSendingMsg1 bob n_a in
-  let (_ , tr_state) = set_state alice sess_id st tr in
-  set_state_state_was_set alice sess_id st tr;
-  assert(state_was_set_some_id tr_state alice (InitiatorSendingMsg1 bob n_a));
-
-  match get_public_key alice global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") bob tr_state with
-    | (None, tr) -> ()
-    | (Some pk_b, tr) -> (
-    
-      let (nonce, tr) = mk_rand PkNonce (long_term_key_label alice) 32 tr in
-      compute_message1_proof tr alice bob pk_b n_a nonce;
-      
   ()
-    )
 
 val prepare_msg2_proof:
   tr:trace ->
@@ -215,16 +191,9 @@ val prepare_msg2_proof:
     trace_invariant tr_out
   ))
 let prepare_msg2_proof tr global_sess_id bob msg_id =
-  match recv_msg msg_id tr with
-  | (None, tr) -> ()
-  | (Some msg, tr) -> (
-    match get_private_key bob global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr with
-    | (None, tr) -> ()
-    | (Some sk_b, tr) -> (
-      decode_message1_proof tr bob msg sk_b
-    )
-  )
+  ()
 
+#push-options "--ifuel 3"
 val send_msg2_proof:
   tr:trace ->
   global_sess_id:nsl_global_sess_ids -> bob:principal -> sess_id:state_id ->
@@ -235,17 +204,8 @@ val send_msg2_proof:
     trace_invariant tr_out
   ))
 let send_msg2_proof tr global_sess_id bob sess_id =
-  match get_state bob sess_id tr with
-  | (Some (ResponderSendingMsg2 alice n_a n_b), tr) -> (
-    assert(state_was_set_some_id tr bob (ResponderSendingMsg2 alice n_a n_b));
-    match get_public_key bob global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") alice tr with
-    | (None, tr) -> ()
-    | (Some pk_a, tr) -> (
-      let (nonce, tr) = mk_rand PkNonce (long_term_key_label bob) 32 tr in
-      compute_message2_proof tr bob {n_a; alice;} pk_a n_b nonce
-    )
-  )
-  | (_, tr) -> ()
+  ()
+#pop-options
 
 val send_msg2__proof:
   tr:trace ->
@@ -257,33 +217,9 @@ val send_msg2__proof:
     trace_invariant tr_out
   ))
 let send_msg2__proof tr global_sess_id bob msg_id =
-  match recv_msg msg_id tr with
-  | (None, tr) -> ()
-  | (Some msg, tr) -> (
-    match get_private_key bob global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr with
-    | (None, tr) -> ()
-    | (Some sk_b, tr) -> (
-      decode_message1_proof tr bob msg sk_b;
-      match decode_message1 bob msg sk_b with
-      | None -> ()
-      | Some msg1 -> (
-      let alice = msg1.alice in
-      let n_a = msg1.n_a in
-    let (n_b, tr) = mk_rand NoUsage (join (principal_label msg1.alice) (principal_label bob)) 32 tr in
-    let (_, tr) = trigger_event bob (Responding alice bob n_a n_b) tr in
-    let st = ResponderSendingMsg2 msg1.alice msg1.n_a n_b in
-    let (sess_id, _) = new_session_id bob tr in
-    let (_, tr_st) = set_state bob sess_id st tr in
-//    set_state_state_was_set bob sess_id st tr_st;
-    assert(state_was_set_some_id tr_st bob st);
-    match get_public_key bob global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") alice tr_st with
-    | (None, tr) -> ()
-    | (Some pk_a, tr) -> (
-      let (nonce, tr) = mk_rand PkNonce (long_term_key_label bob) 32 tr in
-      compute_message2_proof tr bob {n_a; alice;} pk_a n_b nonce
-    )
-  ))
-  )
+  match send_msg2_ global_sess_id bob msg_id tr with
+  | (None, _) -> ()
+  | (Some opt_ids, tr_out) -> ()
 
 val prepare_msg3_proof:
   tr:trace ->
@@ -295,20 +231,9 @@ val prepare_msg3_proof:
     trace_invariant tr_out
   ))
 let prepare_msg3_proof tr global_sess_id alice sess_id msg_id =
-  match recv_msg msg_id tr with
-  | (None, tr) -> ()
-  | (Some msg, tr) -> (
-    match get_private_key alice global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr with
-    | (None, tr) -> ()
-    | (Some sk_a, tr) -> (
-      match get_state alice sess_id tr with
-      | (Some (InitiatorSendingMsg1 bob n_a), tr) -> (
-                decode_message2_proof tr alice bob msg sk_a n_a
-      )
-      | (_, tr) -> ()
-    )
-  )
+  ()
 
+#push-options "--ifuel 4 --fuel 4 --z3rlimit 50"
 val prepare_msg3__proof:
   tr:trace ->
   global_sess_id:nsl_global_sess_ids -> alice:principal -> msg_id:timestamp ->
@@ -319,28 +244,21 @@ val prepare_msg3__proof:
     trace_invariant tr_out
   ))
 let prepare_msg3__proof tr global_sess_id alice msg_id =
-  match recv_msg msg_id tr with
-  | (None, tr) -> ()
-  | (Some msg, tr) -> (
-    match get_private_key alice global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr with
-    | (None, tr) -> ()
-    | (Some sk_a, tr) -> (
-        match decode_message2_ alice msg sk_a with
-        | None -> ()
-        | Some msg2 ->
-        let p = (fun (s:nsl_session) -> 
-    (InitiatorSendingMsg1? s) && 
-    (InitiatorSendingMsg1?.n_a s = msg2.n_a) && 
-    (InitiatorSendingMsg1?.b s = msg2.bob))  in
-        match lookup_state alice p tr with
-        | (None , _) -> ()
-        | (Some (st, sid) , _ ) ->
-                decode_message2_proof tr alice msg2.bob msg sk_a msg2.n_a
-    )
-  )
-
-
-
+  match prepare_msg3_ global_sess_id alice msg_id tr with
+  | (None, _) -> ()
+  | (Some opt_sess_id, tr_out) ->
+      let (Some msg, tr) = recv_msg msg_id tr in
+      let (Some sk_a, tr) = get_private_key alice global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr in
+      let Some msg2 = decode_message2_ alice msg sk_a in
+//       let p = (fun (s:nsl_session) -> 
+//         (InitiatorSendingMsg1? s) && 
+//         (InitiatorSendingMsg1?.n_a s = msg2.n_a) && 
+//         (InitiatorSendingMsg1?.b s = msg2.bob))  in
+// //      let (Some (st, sid) , _ ) = lookup_state alice p tr in
+      decode_message2_proof tr alice msg2.bob msg sk_a msg2.n_a
+
+
+#push-options "--ifuel 3"
 val send_msg3_proof:
   tr:trace ->
   global_sess_id:nsl_global_sess_ids -> alice:principal -> sess_id:state_id ->
@@ -351,19 +269,8 @@ val send_msg3_proof:
     trace_invariant tr_out
   ))
 let send_msg3_proof tr global_sess_id alice sess_id =
-  match get_state alice sess_id tr with
-  | (Some (InitiatorSendingMsg3 bob n_a n_b), tr) -> (
-    assert(state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a n_b));
-    match get_public_key alice global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") bob tr with
-    | (None, tr) -> ()
-    | (Some pk_b, tr) -> (
-      let (nonce, tr) = mk_rand PkNonce (long_term_key_label alice) 32 tr in
-      compute_message3_proof tr alice bob pk_b n_b nonce
-    )
-  )
-  | (_, tr) -> ()
-
-
+  ()
+#pop-options
 
 val send_msg3__proof:
   tr:trace ->
@@ -375,36 +282,30 @@ val send_msg3__proof:
     trace_invariant tr_out
   ))
 let send_msg3__proof tr global_sess_id alice msg_id =
-    match recv_msg msg_id tr with
-  | (None, tr) -> ()
-  | (Some msg, tr) -> (
-    match get_private_key alice global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr with
-    | (None, tr) -> ()
-    | (Some sk_a, tr) -> (
-        match decode_message2_ alice msg sk_a with
-        | None -> ()
-        | Some msg2 -> (
-        let p = (fun (s:nsl_session) -> 
-    (InitiatorSendingMsg1? s) && 
-    (InitiatorSendingMsg1?.n_a s = msg2.n_a) && 
-    (InitiatorSendingMsg1?.b s = msg2.bob))  in
-        match lookup_state alice p tr with
-        | (None , _) -> ()
-        | (Some (st, sid) , _ ) -> (
-                decode_message2_proof tr alice msg2.bob msg sk_a msg2.n_a;
-        let n_b = msg2.n_b in
-        let InitiatorSendingMsg1 bob n_a = st in
-        let new_st = InitiatorSendingMsg3 bob n_a n_b in
-        let (_, tr_state) = set_state alice sid new_st tr in
-        assert(state_was_set_some_id tr_state alice new_st);
-    match get_public_key alice global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") bob tr_state with
-    | (None, tr) -> ()
-    | (Some pk_b, tr) -> (
+  match send_msg3_ global_sess_id alice msg_id tr with
+  | (None, tr_out) -> (
+      admit()
+  )
+  | (Some opt_ids, tr_out) -> (
+      let (Some msg, tr) = recv_msg msg_id tr in
+      let (Some sk_a, tr) =  get_private_key alice global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr in
+      let Some msg2 = decode_message2_ alice msg sk_a in
+      let p = (fun (s:nsl_session) -> 
+        (InitiatorSendingMsg1? s) && 
+        (InitiatorSendingMsg1?.n_a s = msg2.n_a) && 
+        (InitiatorSendingMsg1?.b s = msg2.bob))  in
+      let (Some (st, sid) , _ ) = lookup_state alice p tr in
+      decode_message2_proof tr alice msg2.bob msg sk_a msg2.n_a;
+      let n_b = msg2.n_b in
+      let InitiatorSendingMsg1 bob n_a = st in
+      let new_st = InitiatorSendingMsg3 bob n_a n_b in
+      let (_, tr_state) = set_state alice sid new_st tr in
+      assert(state_was_set_some_id tr_state alice new_st);
+      let (Some pk_b, tr) = get_public_key alice global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") bob tr_state in
       let (nonce, tr) = mk_rand PkNonce (long_term_key_label alice) 32 tr in
       compute_message3_proof tr alice bob pk_b n_b nonce
-    )
-  ))
- ))
+      )
+  
 
 
 val event_respond1_injective:
@@ -433,38 +334,30 @@ val receive_msg3_proof:
     trace_invariant tr_out
   ))
 let receive_msg3_proof tr global_sess_id bob sess_id msg_id =
-  match recv_msg msg_id tr with
-  | (None, tr) -> ()
-  | (Some msg, tr) -> (
-    match get_private_key bob global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr with
-    | (None, tr) -> ()
-    | (Some sk_b, tr) -> (
-        match decode_message3_ msg sk_b with
-        | None -> ()
-        | Some msg3 -> (
-            let p = (fun (s:nsl_session) -> 
-    (ResponderSendingMsg2? s) && 
-    (ResponderSendingMsg2?.n_b s = msg3.n_b)) in
-           match lookup_state bob p tr with
-           | (None, _ ) -> ()
-           | (Some (st, id), _) ->  (
-           let ResponderSendingMsg2 alice n_a n_b = st in
-            assert(event_triggered tr bob (Responding alice bob n_a n_b));
-             
-            assert(is_publishable tr n_b ==> is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob));
-            introduce ~(is_publishable tr n_b) ==> 
-            state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a n_b)
-            with _. (
-              decode_message3__proof tr alice bob msg sk_b;
-              eliminate exists alice' n_a'. get_label tr n_b `can_flow tr` (principal_label alice') /\ 
-              state_was_set_some_id tr alice' (InitiatorSendingMsg3 bob n_a' n_b)
-              returns _
-              with _. (
-                assert(event_triggered tr bob (Responding alice' bob n_a' n_b));
-                event_respond1_injective tr alice alice' bob n_a n_a' n_b
-              
-              )
-
-            )
-           )
-   )))
+  match receive_msg3 global_sess_id bob msg_id tr with
+  | (None, _) -> ()
+  | (Some opt_sess_id, tr_out) -> 
+      let (Some msg, tr) = recv_msg msg_id tr in
+      let (Some sk_b, tr) = get_private_key bob global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr in
+      let Some msg3 = decode_message3_ bob msg sk_b in
+      let p = (fun (s:nsl_session) -> 
+        (ResponderSendingMsg2? s) && 
+        (ResponderSendingMsg2?.n_b s = msg3.n_b)) in
+      let (Some (st, id), _) = lookup_state bob p tr in
+      let ResponderSendingMsg2 alice n_a n_b = st in
+      assert(event_triggered tr bob (Responding alice bob n_a n_b));
+
+      assert(is_publishable tr n_b ==> is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob));
+      introduce ~(is_publishable tr n_b) ==> 
+      state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a n_b)
+      with _. (
+        decode_message3__proof tr bob msg sk_b;
+        eliminate exists alice' n_a'. get_label tr n_b `can_flow tr` (principal_label alice') /\ 
+        state_was_set_some_id tr alice' (InitiatorSendingMsg3 bob n_a' n_b)
+        returns _
+        with _. (
+          assert(event_triggered tr bob (Responding alice' bob n_a' n_b));
+          event_respond1_injective tr alice alice' bob n_a n_a' n_b
+
+        )
+      )
diff --git a/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Stateful.fst b/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Stateful.fst
index adbb323..920932c 100644
--- a/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Stateful.fst
+++ b/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Stateful.fst
@@ -159,15 +159,16 @@ let prepare_msg3_ global_sess_id alice msg_id =
     (InitiatorSendingMsg1? s) && 
     (InitiatorSendingMsg1?.n_a s = msg2.n_a) && 
     (InitiatorSendingMsg1?.b s = msg2.bob))  in
-  let* tr = get_trace in
-  let (opt_st, _) = lookup_state #nsl_session alice p tr in
-  match opt_st with
-  | None -> return None
-  | Some (st, sid ) -> (
+  // let* tr = get_trace in
+  let*? (st, sid) = lookup_state #nsl_session alice p in
+  guard_tr (p st);*?
+  // match opt_st with
+  // | None -> return None
+  // | Some (st, sid ) -> (
       let InitiatorSendingMsg1 bob n_a = st in
       set_state alice sid (InitiatorSendingMsg3 bob n_a msg2.n_b <: nsl_session);*
       return (Some sid)
-  )
+  // )
 
 
 val send_msg3: nsl_global_sess_ids -> principal -> state_id -> traceful (option timestamp)
@@ -191,22 +192,23 @@ let send_msg3_ global_sess_id alice msg_id =
     (InitiatorSendingMsg1? s) && 
     (InitiatorSendingMsg1?.n_a s = msg2.n_a) && 
     (InitiatorSendingMsg1?.b s = msg2.bob))  in
-  let* tr = get_trace in
-  let (opt_st, _) = lookup_state #nsl_session alice p tr in
-  match opt_st with
-  | None -> return None
-  | Some (st, sid ) -> (
-      let n_b = msg2.n_b in
-      let InitiatorSendingMsg1 bob n_a = st in
-      let st = InitiatorSendingMsg3 bob n_a n_b in
-      set_state alice sid st;*
+  //let* tr = get_trace in
+  let*? (st, sid) = lookup_state #nsl_session alice p in
+  // match opt_st with
+  // | None -> return None
+  // | Some (st, sid ) -> (
+  let n_b = msg2.n_b in
+  guard_tr(p st);*?
+  let InitiatorSendingMsg1 bob n_a = st in
+  let st = InitiatorSendingMsg3 bob n_a n_b in
+  set_state alice sid st;*
   
   let*? pk_b = get_public_key alice global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") bob in
   let* nonce = mk_rand PkNonce (long_term_key_label alice) 32 in
   let msg3 = compute_message3 alice bob pk_b n_b nonce in
   let* msg_id = send_msg msg3 in
   return (Some (msg_id, sid))
-  )
+  // )
 
 val prepare_msg4: nsl_global_sess_ids -> principal -> state_id -> timestamp -> traceful (option unit)
 let prepare_msg4 global_sess_id bob sess_id msg_id =
@@ -224,16 +226,12 @@ let receive_msg3 global_sess_id bob msg_id =
   let*? msg = recv_msg msg_id in
   let*? sk_b = get_private_key bob global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") in
 
-  let*? msg3: message3 = return (decode_message3_ msg sk_b) in
+  let*? msg3: message3 = return (decode_message3_ bob msg sk_b) in
   let p = (fun (s:nsl_session) -> 
     (ResponderSendingMsg2? s) && 
     (ResponderSendingMsg2?.n_b s = msg3.n_b)) in
-  let* tr = get_trace in
-  let (opt_st, _) = lookup_state #nsl_session bob p tr in
-  match opt_st with
-  | None -> return None
-  | Some (st, sid ) -> (
-         let ResponderSendingMsg2 alice n_a n_b = st in
-         set_state bob sid (ResponderReceivedMsg3 alice n_a n_b <: nsl_session);*
+  let*? (st, sid) = lookup_state #nsl_session bob p in
+  guard_tr (p st);*?
+  let ResponderSendingMsg2 alice n_a n_b = st in
+  set_state bob sid (ResponderReceivedMsg3 alice n_a n_b <: nsl_session);*
   return (Some ())
-  )
diff --git a/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Total.Proof.fst b/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Total.Proof.fst
index 146cd88..63cb127 100644
--- a/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Total.Proof.fst
+++ b/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Total.Proof.fst
@@ -93,6 +93,7 @@ let rand_generated_before tr b =
 
 
 val compute_message1_proof:
+  {|protocol_invariants|} ->
   tr:trace ->
   alice:principal -> bob:principal -> pk_b:bytes -> n_a:bytes -> nonce:bytes ->
   Lemma
@@ -109,7 +110,9 @@ val compute_message1_proof:
     is_public_key_for tr pk_b (LongTermPkEncKey "NSL.PublicKey") bob
   )
   (ensures is_publishable tr (compute_message1 alice bob pk_b n_a nonce))
-let compute_message1_proof tr alice bob pk_b n_a nonce =
+  [SMTPat (trace_invariant tr);
+    SMTPat (compute_message1 alice bob pk_b n_a nonce)]
+let compute_message1_proof #invs tr alice bob pk_b n_a nonce =
   let msg = Msg1 {n_a; alice;} in
   serialize_wf_lemma message (is_knowable_by (long_term_key_label alice) tr) msg;
   serialize_wf_lemma message (is_knowable_by (long_term_key_label bob) tr) msg
@@ -121,6 +124,7 @@ let compute_message1_proof tr alice bob pk_b n_a nonce =
 // - if the message was encrypted by an honest principal, this follows from the encryption predicate
 #push-options "--ifuel 1 --fuel 0 --z3rlimit 25"
 val decode_message1_proof:
+  {|protocol_invariants|} ->
   tr:trace ->
   bob:principal -> msg_cipher:bytes -> sk_b:bytes ->
   Lemma
@@ -141,7 +145,9 @@ val decode_message1_proof:
       )
     )
   ))
-let decode_message1_proof tr bob msg_cipher sk_b =
+  [SMTPat (trace_invariant tr);
+    SMTPat (decode_message1 bob msg_cipher sk_b)]
+let decode_message1_proof #invs tr bob msg_cipher sk_b =
   match decode_message1 bob msg_cipher sk_b with
   | None -> ()
   | Some msg1 ->
@@ -151,6 +157,7 @@ let decode_message1_proof tr bob msg_cipher sk_b =
 #pop-options
 
 val compute_message2_proof:
+  {|protocol_invariants|} ->
   tr:trace ->
   bob:principal -> msg1:message1 -> pk_a:bytes -> n_b:bytes -> nonce:bytes ->
   Lemma
@@ -171,7 +178,9 @@ val compute_message2_proof:
   (ensures
     is_publishable tr (compute_message2 bob msg1 pk_a n_b nonce)
   )
-let compute_message2_proof tr bob msg1 pk_a n_b nonce =
+  [SMTPat (trace_invariant tr);
+    SMTPat (compute_message2 bob msg1 pk_a n_b nonce)]
+let compute_message2_proof #invs tr bob msg1 pk_a n_b nonce =
   let msg = Msg2 {n_a = msg1.n_a;  n_b; bob;} in
   serialize_wf_lemma message (is_knowable_by (principal_label msg1.alice) tr) msg;
   serialize_wf_lemma message (is_knowable_by (principal_label bob) tr) msg
@@ -183,6 +192,7 @@ let compute_message2_proof tr bob msg1 pk_a n_b nonce =
 // (proved with the encryption predicate)
 #push-options "--ifuel 1 --fuel 0 --z3rlimit 25"
 val decode_message2_proof:
+  {|protocol_invariants|} ->
   tr:trace ->
   alice:principal -> bob:principal -> msg_cipher:bytes -> sk_a:bytes -> n_a:bytes ->
   Lemma
@@ -208,7 +218,9 @@ val decode_message2_proof:
       )
     )
   ))
-let decode_message2_proof tr alice bob msg_cipher sk_a n_a =
+  [SMTPat (trace_invariant tr);
+    SMTPat (decode_message2 alice bob msg_cipher sk_a n_a)]
+let decode_message2_proof #invs tr alice bob msg_cipher sk_a n_a =
   match decode_message2 alice bob msg_cipher sk_a n_a with
   | None -> ()
   | Some msg2 -> (
@@ -223,6 +235,7 @@ let decode_message2_proof tr alice bob msg_cipher sk_a n_a =
 #pop-options
 
 val compute_message3_proof:
+  {|protocol_invariants|} ->
   tr:trace ->
   alice:principal -> bob:principal -> pk_b:bytes -> n_b:bytes -> nonce:bytes ->
   Lemma
@@ -241,7 +254,9 @@ val compute_message3_proof:
   (ensures
     is_publishable tr (compute_message3 alice bob pk_b n_b nonce)
   )
-let compute_message3_proof tr alice bob pk_b n_b nonce =
+  [SMTPat (trace_invariant tr);
+    SMTPat (compute_message3 alice bob pk_b n_b nonce)]
+let compute_message3_proof #invs tr alice bob pk_b n_b nonce =
   let msg = Msg3 {n_b;} in
   serialize_wf_lemma message (is_knowable_by (principal_label alice) tr) msg;
   serialize_wf_lemma message (is_knowable_by (principal_label bob) tr) msg;
@@ -253,6 +268,7 @@ let compute_message3_proof tr alice bob pk_b n_b nonce =
 // (proved with the encryption predicate)
 #push-options "--ifuel 1 --fuel 0 --z3rlimit 25"
 val decode_message3_proof:
+  {|protocol_invariants|} ->
   tr:trace ->
   alice:principal -> bob:principal -> msg_cipher:bytes -> sk_b:bytes -> n_b:bytes ->
   Lemma
@@ -275,7 +291,9 @@ val decode_message3_proof:
       ))
     )
   ))
-let decode_message3_proof tr alice bob msg_cipher sk_b n_b =
+  [SMTPat (trace_invariant tr);
+    SMTPat (decode_message3 alice bob msg_cipher sk_b n_b)]
+let decode_message3_proof #invs tr alice bob msg_cipher sk_b n_b =
   match decode_message3 alice bob msg_cipher sk_b n_b with
   | None -> ()
   | Some msg3 -> (
@@ -287,8 +305,9 @@ let decode_message3_proof tr alice bob msg_cipher sk_b n_b =
 
 #push-options "--ifuel 1 --fuel 0 --z3rlimit 25"
 val decode_message3__proof:
+  {|protocol_invariants|} ->
   tr:trace ->
-  alice:principal -> bob:principal -> msg_cipher:bytes -> sk_b:bytes ->
+  bob:principal -> msg_cipher:bytes -> sk_b:bytes ->
   Lemma
   (requires
     // From the PrivateKeys invariant
@@ -297,7 +316,7 @@ val decode_message3__proof:
     bytes_invariant tr msg_cipher
   )
   (ensures (
-    match decode_message3_ msg_cipher sk_b with
+    match decode_message3_ bob msg_cipher sk_b with
     | None -> True
     | Some msg3 -> (
       (is_publishable tr msg3.n_b)
@@ -308,8 +327,10 @@ val decode_message3__proof:
       ))
     )
   ))
-let decode_message3__proof tr alice bob msg_cipher sk_b =
-  match decode_message3_ msg_cipher sk_b with
+  [SMTPat (trace_invariant tr);
+    SMTPat (decode_message3_ bob msg_cipher sk_b)]
+let decode_message3__proof #invs tr bob msg_cipher sk_b =
+  match decode_message3_ bob msg_cipher sk_b with
   | None -> ()
   | Some msg3 -> (
     let Some msg = pk_dec sk_b msg_cipher in
diff --git a/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Total.fst b/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Total.fst
index 0afa723..a11f725 100644
--- a/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Total.fst
+++ b/examples/nsl_pk_no_events_lookup/DY.Example.NSL.Protocol.Total.fst
@@ -106,7 +106,7 @@ let decode_message2 alice bob msg2_cipher sk_a n_a =
   Some msg2
 
 
-val decode_message2_: principal  -> bytes -> bytes -> option (message2)
+val decode_message2_: principal -> bytes -> bytes -> option (message2)
 let decode_message2_ alice msg2_cipher sk_a =
   let? msg2_plain = pk_dec sk_a msg2_cipher in
   let? msg2 = parse _ msg2_plain in
@@ -134,8 +134,8 @@ let decode_message3 alice bob msg_cipher sk_b n_b =
   guard (n_b = msg3.n_b);?
   Some msg3
 
-val decode_message3_: bytes -> bytes -> option (message3)
-let decode_message3_ msg_cipher sk_b =
+val decode_message3_: principal -> bytes -> bytes -> option (message3)
+let decode_message3_ bob msg_cipher sk_b =
   let? msg_plain = pk_dec sk_b msg_cipher in
   let? msg = parse _ msg_plain in
   guard (Msg3? msg);?