diff --git a/src/core/DY.Core.Trace.Base.fst b/src/core/DY.Core.Trace.Base.fst
index bdadb05..79e6a0a 100644
--- a/src/core/DY.Core.Trace.Base.fst
+++ b/src/core/DY.Core.Trace.Base.fst
@@ -254,6 +254,20 @@ val event_at_grows:
   [SMTPat (event_at tr1 i e); SMTPat (tr1 <$ tr2)]
 let event_at_grows #label_t tr1 tr2 i e = ()
 
+val last_entry_exists:
+  #label_t:Type ->
+  tr:trace_ label_t ->
+  Lemma
+    (requires Snoc? tr )
+    (ensures (
+       let Snoc _ last = tr in
+       event_exists tr last
+    ))
+    [SMTPat (Snoc? tr)]
+let last_entry_exists tr = 
+  let Snoc _ last = tr in
+  assert(event_at tr (DY.Core.Trace.Base.length tr - 1) last)
+
 /// Shorthand predicates.
 
 /// Has a message been sent on the network?
diff --git a/src/core/DY.Core.Trace.Manipulation.fst b/src/core/DY.Core.Trace.Manipulation.fst
index 09a14fe..b4f630e 100644
--- a/src/core/DY.Core.Trace.Manipulation.fst
+++ b/src/core/DY.Core.Trace.Manipulation.fst
@@ -115,6 +115,15 @@ let add_event e tr =
   norm_spec [zeta; delta_only [`%prefix]] (prefix #label);
   ((), Snoc tr e)
 
+val add_event_event_exists:
+  e:trace_event -> tr:trace ->
+  Lemma
+  (ensures (
+    let ((), tr_out) = add_event e tr in
+    event_exists tr_out e
+  ))
+let add_event_event_exists e tr = ()
+
 /// Adding a trace event preserves the trace invariant
 /// when the trace event satisfy the invariant.
 
@@ -128,8 +137,7 @@ val add_event_invariant:
   )
   (ensures (
     let ((), tr_out) = add_event e tr in
-    trace_invariant tr_out /\
-    event_exists tr_out e
+    trace_invariant tr_out
   ))
 let add_event_invariant #invs e tr =
   norm_spec [zeta; delta_only [`%trace_invariant]] (trace_invariant)
@@ -152,6 +160,18 @@ let send_msg msg =
   add_event (MsgSent msg);*
   return time
 
+val send_msg_msg_event:
+  msg:bytes -> tr:trace ->
+  Lemma
+  (ensures (
+    let (i, tr_out) = send_msg msg tr in
+    event_at tr_out i (MsgSent msg)
+  ))
+ [SMTPat (send_msg msg tr);]
+let send_msg_msg_event msg tr =
+ reveal_opaque (`%send_msg) (send_msg)
+
+
 /// Sending a message on the network preserves the trace invariant
 /// when the message is publishable.
 
@@ -165,8 +185,7 @@ val send_msg_invariant:
   )
   (ensures (
     let (i, tr_out) = send_msg msg tr in
-    trace_invariant tr_out /\
-    event_at tr_out i (MsgSent msg)
+    trace_invariant tr_out
   ))
   [SMTPat (send_msg msg tr); SMTPat (trace_invariant tr)]
 let send_msg_invariant #invs msg tr =
@@ -186,6 +205,18 @@ let recv_msg i =
   else
     return None
 
+
+val recv_msg_same_trace:
+  i:timestamp -> tr:trace ->
+  Lemma
+  (ensures (
+    let (opt_msg, tr_out) = recv_msg i tr in
+    tr_out == tr
+  ))
+  [SMTPat (recv_msg i tr);]
+let recv_msg_same_trace i tr =
+  reveal_opaque (`%recv_msg) recv_msg
+
 /// When the trace invariant holds,
 /// received messages are publishable.
 
@@ -196,11 +227,9 @@ val recv_msg_invariant:
   (requires trace_invariant tr)
   (ensures (
     let (opt_msg, tr_out) = recv_msg i tr in
-    tr_out == tr /\ (
       match opt_msg with
       | None -> True
       | Some msg -> is_publishable tr msg
-    )
   ))
   [SMTPat (recv_msg i tr);
    SMTPat (trace_invariant tr)
@@ -252,9 +281,22 @@ let mk_rand usg lab len =
   add_event (RandGen usg lab len);*
   return (Rand len time)
 
+
+val mk_rand_rand_gen_at_end:
+  usg:usage -> lab:label -> len:nat{len <> 0} -> tr:trace ->
+  Lemma
+  (ensures (
+    let (b, tr_out) = mk_rand usg lab len tr in
+    1 <= DY.Core.Trace.Base.length tr_out /\
+    rand_generated_at tr_out (DY.Core.Trace.Base.length tr_out - 1) b
+  ))
+  [SMTPat (mk_rand usg lab len tr);]
+let mk_rand_rand_gen_at_end usg lab len tr =
+  reveal_opaque (`%mk_rand) (mk_rand)
+
+
 /// Generating a random bytestrings always preserve the trace invariant.
 
-#push-options "--z3rlimit 25"
 val mk_rand_trace_invariant:
   {|protocol_invariants|} ->
   usg:usage -> lab:label -> len:nat{len <> 0} -> tr:trace ->
@@ -262,15 +304,12 @@ val mk_rand_trace_invariant:
   (requires trace_invariant tr)
   (ensures (
     let (b, tr_out) = mk_rand usg lab len tr in
-    trace_invariant tr_out /\
-    1 <= DY.Core.Trace.Base.length tr_out /\
-    rand_generated_at tr_out (DY.Core.Trace.Base.length tr_out - 1) b
+    trace_invariant tr_out
   ))
   [SMTPat (mk_rand usg lab len tr); SMTPat (trace_invariant tr)]
 let mk_rand_trace_invariant #invs usg lab len tr =
   add_event_invariant (RandGen usg lab len) tr;
   reveal_opaque (`%mk_rand) (mk_rand)
-#pop-options
 
 /// Random bytestrings satisfy the bytes invariant.
 
@@ -418,7 +457,7 @@ let get_state prin sess_id =
 
 /// Obtaining a new state identifier do not change the trace.
 
-val new_session_id_invariant:
+val new_session_id_same_trace:
   prin:principal -> tr:trace ->
   Lemma
   (ensures (
@@ -426,13 +465,25 @@ val new_session_id_invariant:
     tr == tr_out
   ))
   [SMTPat (new_session_id prin tr)]
-let new_session_id_invariant prin tr =
+let new_session_id_same_trace prin tr =
   normalize_term_spec new_session_id
 
+
+val set_state_state_was_set:
+  prin:principal -> sess_id:state_id -> content:bytes -> tr:trace ->
+  Lemma
+  (ensures (
+    let ((), tr_out) = set_state prin sess_id content tr in
+    state_was_set tr_out prin sess_id content
+  ))
+  [SMTPat (set_state prin sess_id content tr);]
+let set_state_state_was_set prin sess_id content tr =
+  normalize_term_spec set_state
+
+
 /// Storing a state preserves the trace invariant
 /// when the state satisfy the state predicate.
 
-#push-options "--z3rlimit 15"
 val set_state_invariant:
   {|protocol_invariants|} ->
   prin:principal -> sess_id:state_id -> content:bytes -> tr:trace ->
@@ -443,71 +494,59 @@ val set_state_invariant:
   )
   (ensures (
     let ((), tr_out) = set_state prin sess_id content tr in
-    trace_invariant tr_out /\
-    state_was_set tr_out prin sess_id content
+    trace_invariant tr_out
   ))
   [SMTPat (set_state prin sess_id content tr); SMTPat (trace_invariant tr)]
 let set_state_invariant #invs prin sess_id content tr =
   add_event_invariant (SetState prin sess_id content) tr;
   normalize_term_spec set_state
-#pop-options
 
-val get_state_aux_state_invariant:
-  {|protocol_invariants|} ->
+val get_state_same_trace:
+  prin:principal -> sess_id:state_id -> tr:trace ->
+  Lemma
+  (ensures (
+    let (opt_content, tr_out) = get_state prin sess_id tr in
+    tr == tr_out
+  ))
+  [SMTPat (get_state prin sess_id tr);]
+let get_state_same_trace prin sess_id tr =
+  reveal_opaque (`%get_state) get_state
+
+
+val get_state_aux_state_was_set:
   prin:principal -> sess_id:state_id -> tr:trace ->
   Lemma
-  (requires
-    trace_invariant tr
-  )
   (ensures (
     match get_state_aux prin sess_id tr with
     | None -> True
-    | Some content -> state_pred.pred tr prin sess_id content
+    | Some content -> 
+        state_was_set tr prin sess_id content
   ))
-let rec get_state_aux_state_invariant #invs prin sess_id tr =
-  reveal_opaque (`%grows) (grows #label);
-  norm_spec [zeta; delta_only [`%trace_invariant]] (trace_invariant);
-  norm_spec [zeta; delta_only [`%prefix]] (prefix #label);
-  match tr with
+let rec get_state_aux_state_was_set prin sess_id tr =
+   match tr with
   | Nil -> ()
   | Snoc tr_init (SetState prin' sess_id' content) -> (
-    if prin = prin' && sess_id = sess_id' then (
-      state_pred.pred_later tr_init tr prin sess_id content
-    ) else (
-      get_state_aux_state_invariant prin sess_id tr_init;
-      match get_state_aux prin sess_id tr_init with
-      | None -> ()
-      | Some content -> state_pred.pred_later tr_init tr prin sess_id content
-    )
+    if prin = prin' && sess_id = sess_id' 
+    then ()
+    else get_state_aux_state_was_set prin sess_id tr_init
   )
   | Snoc tr_init _ ->
-    get_state_aux_state_invariant prin sess_id tr_init;
-    match get_state_aux prin sess_id tr_init with
-    | None -> ()
-    | Some content -> state_pred.pred_later tr_init tr prin sess_id content
-
-/// When the trace invariant holds,
-/// retrieved states satisfy the state predicate.
+         get_state_aux_state_was_set prin sess_id tr_init
 
-val get_state_state_invariant:
-  {|protocol_invariants|} ->
+val get_state_state_was_set:
   prin:principal -> sess_id:state_id -> tr:trace ->
   Lemma
-  (requires
-    trace_invariant tr
-  )
   (ensures (
     let (opt_content, tr_out) = get_state prin sess_id tr in
-    tr == tr_out /\ (
-      match opt_content with
-      | None -> True
-      | Some content -> state_pred.pred tr prin sess_id content
-    )
+    match opt_content with
+    | None -> True
+    | Some content ->
+        state_was_set tr prin sess_id content
   ))
-  [SMTPat (get_state prin sess_id tr); SMTPat (trace_invariant tr)]
-let get_state_state_invariant #invs prin sess_id tr =
-  normalize_term_spec get_state;
-  get_state_aux_state_invariant prin sess_id tr
+  [SMTPat (get_state prin sess_id tr)]
+let get_state_state_was_set prin sess_id tr =
+  reveal_opaque (`%get_state) get_state;
+  get_state_aux_state_was_set prin sess_id tr
 
 (*** Event triggering ***)
 
@@ -518,6 +557,17 @@ val trigger_event: principal -> string -> bytes -> traceful unit
 let trigger_event prin tag content =
   add_event (Event prin tag content)
 
+val trigger_event_event_triggered:
+  prin:principal -> tag:string -> content:bytes -> tr:trace ->
+  Lemma
+  (ensures (
+    let ((), tr_out) = trigger_event prin tag content tr in
+    event_triggered tr_out prin tag content
+  ))
+  [SMTPat (trigger_event prin tag content tr);]
+let trigger_event_event_triggered prin tag content tr =
+  reveal_opaque (`%trigger_event) trigger_event
+
 /// Triggering a protocol event preserves the trace invariant
 /// when the protocol event satisfy the event predicate.
 
@@ -531,8 +581,7 @@ val trigger_event_trace_invariant:
   )
   (ensures (
     let ((), tr_out) = trigger_event prin tag content tr in
-    trace_invariant tr_out /\
-    event_triggered tr_out prin tag content
+    trace_invariant tr_out
   ))
   [SMTPat (trigger_event prin tag content tr); SMTPat (trace_invariant tr)]
 let trigger_event_trace_invariant #invs prin tag content tr =
diff --git a/src/lib/event/DY.Lib.Event.Typed.fst b/src/lib/event/DY.Lib.Event.Typed.fst
index 9db19f0..9abb856 100644
--- a/src/lib/event/DY.Lib.Event.Typed.fst
+++ b/src/lib/event/DY.Lib.Event.Typed.fst
@@ -137,6 +137,19 @@ val event_triggered:
 let event_triggered #a #ev tr prin e =
   exists i. event_triggered_at tr i prin e
 
+val trigger_event_event_triggered:
+  #a:Type -> {|ev:event a|} ->
+  prin:principal -> e:a -> tr:trace ->
+  Lemma
+  (ensures (
+    let ((), tr_out) = trigger_event prin e tr in
+    event_triggered tr_out prin e
+  ))
+  [SMTPat (trigger_event #a #ev prin e tr);]
+let trigger_event_event_triggered #a #ev prin e tr =
+  reveal_opaque (`%trigger_event) (trigger_event #a);
+  reveal_opaque (`%event_triggered_at) (event_triggered_at #a)
+
 val trigger_event_trace_invariant:
   {|protocol_invariants|} ->
   #a:Type -> {|ev:event a|} ->
@@ -150,8 +163,7 @@ val trigger_event_trace_invariant:
   )
   (ensures (
     let ((), tr_out) = trigger_event prin e tr in
-    trace_invariant tr_out /\
-    event_triggered tr_out prin e
+    trace_invariant tr_out
   ))
   [SMTPat (trigger_event prin e tr);
    SMTPat (has_event_pred epred);
@@ -159,9 +171,22 @@ val trigger_event_trace_invariant:
 let trigger_event_trace_invariant #invs #a #ev epred prin e tr =
   reveal_opaque (`%has_compiled_event_pred) (has_compiled_event_pred);
   reveal_opaque (`%trigger_event) (trigger_event #a);
-  reveal_opaque (`%event_triggered_at) (event_triggered_at #a);
   local_eq_global_lemma split_event_pred_params event_pred ev.tag (compile_event_pred epred) (tr, prin, ev.tag, serialize _ e) ev.tag (tr, prin, serialize _ e)
 
+
+val event_triggered_at_on_trace:
+  #a:Type -> {|ev:event a|} ->
+  tr:trace ->
+  i:timestamp -> prin:principal -> e:a ->
+  Lemma
+  (requires
+    event_triggered_at tr i prin e
+  )
+  (ensures i < DY.Core.Trace.Base.length tr)
+  [SMTPat (event_triggered_at #a #ev tr i prin e)]
+let event_triggered_at_on_trace #a #ev  tr i prin e =
+  reveal_opaque (`%event_triggered_at) (event_triggered_at #a)
+
 val event_triggered_at_implies_pred:
   {|protocol_invariants|} ->
   #a:Type -> {|ev:event a|} ->
@@ -173,7 +198,7 @@ val event_triggered_at_implies_pred:
     has_event_pred epred /\
     trace_invariant tr
   )
-  (ensures i <= DY.Core.Trace.Base.length tr /\ epred (prefix tr i) prin e)
+  (ensures epred (prefix tr i) prin e)
   [SMTPat (event_triggered_at tr i prin e);
    SMTPat (has_event_pred epred);
    SMTPat (trace_invariant tr);
@@ -201,7 +226,6 @@ val event_triggered_at_implies_trace_event_at:
   Lemma
   (requires event_triggered_at tr i prin e)
   (ensures
-    i < DY.Core.Trace.Base.length tr /\
     get_event_at tr i == Event prin ev.tag (serialize a e) /\
     parse #bytes a (serialize a e) == Some e
   )
diff --git a/src/lib/state/DY.Lib.State.Map.fst b/src/lib/state/DY.Lib.State.Map.fst
index fd29855..7326dfd 100644
--- a/src/lib/state/DY.Lib.State.Map.fst
+++ b/src/lib/state/DY.Lib.State.Map.fst
@@ -237,6 +237,20 @@ let add_key_value_invariant #invs #key_t #value_t #mt mpred prin sess_id key val
   reveal_opaque (`%add_key_value) (add_key_value #key_t #value_t)
 #pop-options
 
+val find_value_same_trace:
+  #key_t:eqtype -> #value_t:Type0 -> {|map_types key_t value_t|} ->
+  prin:principal -> sess_id:state_id ->
+  key:key_t ->
+  tr:trace ->
+  Lemma
+  (ensures (
+    let (opt_value, tr_out) = find_value #_ #value_t prin sess_id key tr in
+    tr_out == tr
+  ))
+  [SMTPat (find_value #key_t #value_t prin sess_id key tr)]
+let find_value_same_trace #key_t #value_t #mt prin sess_id key tr =
+  reveal_opaque (`%find_value) (find_value #key_t #value_t)
+
 val find_value_invariant:
   {|protocol_invariants|} ->
   #key_t:eqtype -> #value_t:Type0 -> {|map_types key_t value_t|} ->
@@ -251,13 +265,11 @@ val find_value_invariant:
   )
   (ensures (
     let (opt_value, tr_out) = find_value prin sess_id key tr in
-    tr_out == tr /\ (
       match opt_value with
       | None -> True
       | Some value -> (
         mpred.pred tr prin sess_id key value
       )
-    )
   ))
   [SMTPat (find_value #key_t #value_t prin sess_id key tr);
    SMTPat (has_map_session_invariant mpred);
diff --git a/src/lib/state/DY.Lib.State.PKI.fst b/src/lib/state/DY.Lib.State.PKI.fst
index 4989517..802bf37 100644
--- a/src/lib/state/DY.Lib.State.PKI.fst
+++ b/src/lib/state/DY.Lib.State.PKI.fst
@@ -117,6 +117,18 @@ val install_public_key_invariant:
 let install_public_key_invariant #invs prin sess_id pk_type who pk tr =
   reveal_opaque (`%install_public_key) (install_public_key)
 
+
+val get_public_key_same_trace:
+  prin:principal -> sess_id:state_id -> pk_type:long_term_key_type -> who:principal -> tr:trace ->
+  Lemma
+  (ensures (
+    let (opt_public_key, tr_out) = get_public_key prin sess_id pk_type who tr in
+    tr_out == tr
+  ))
+  [SMTPat (get_public_key prin sess_id pk_type who tr);]
+let get_public_key_same_trace prin sess_id pk_type who tr =
+  reveal_opaque (`%get_public_key) (get_public_key)
+
 val get_public_key_invariant:
   {|protocol_invariants|} ->
   prin:principal -> sess_id:state_id -> pk_type:long_term_key_type -> who:principal -> tr:trace ->
@@ -127,12 +139,10 @@ val get_public_key_invariant:
   )
   (ensures (
     let (opt_public_key, tr_out) = get_public_key prin sess_id pk_type who tr in
-    tr_out == tr /\ (
-      match opt_public_key with
-      | None -> True
-      | Some public_key ->
+    match opt_public_key with
+    | None -> True
+    | Some public_key ->
         is_public_key_for tr public_key pk_type who
-    )
   ))
   [SMTPat (get_public_key prin sess_id pk_type who tr);
    SMTPat (has_pki_invariant);
diff --git a/src/lib/state/DY.Lib.State.PrivateKeys.fst b/src/lib/state/DY.Lib.State.PrivateKeys.fst
index 308dd35..24171b0 100644
--- a/src/lib/state/DY.Lib.State.PrivateKeys.fst
+++ b/src/lib/state/DY.Lib.State.PrivateKeys.fst
@@ -173,6 +173,18 @@ val generate_private_key_invariant:
 let generate_private_key_invariant #invs prin sess_id sk_type tr =
   reveal_opaque (`%generate_private_key) (generate_private_key)
 
+val get_private_key_same_trace:
+  prin:principal -> sess_id:state_id -> pk_type:long_term_key_type -> tr:trace ->
+  Lemma
+  (ensures (
+    let (opt_private_key, tr_out) = get_private_key prin sess_id pk_type tr in
+    tr_out == tr
+  ))
+  [SMTPat (get_private_key prin sess_id pk_type tr);]
+let get_private_key_same_trace prin sess_id pk_type tr =
+  reveal_opaque (`%get_private_key) (get_private_key)
+
+
 val get_private_key_invariant:
   {|protocol_invariants|} ->
   prin:principal -> sess_id:state_id -> pk_type:long_term_key_type -> tr:trace ->
@@ -183,12 +195,10 @@ val get_private_key_invariant:
   )
   (ensures (
     let (opt_private_key, tr_out) = get_private_key prin sess_id pk_type tr in
-    tr_out == tr /\ (
-      match opt_private_key with
-      | None -> True
-      | Some private_key ->
+    match opt_private_key with
+    | None -> True
+    | Some private_key ->
         is_private_key_for tr private_key pk_type prin
-    )
   ))
   [SMTPat (get_private_key prin sess_id pk_type tr);
    SMTPat (has_private_keys_invariant);
@@ -196,6 +206,19 @@ val get_private_key_invariant:
 let get_private_key_invariant #invs prin sess_id pk_type tr =
   reveal_opaque (`%get_private_key) (get_private_key)
 
+
+val compute_public_key_same_trace:
+  prin:principal -> sess_id:state_id -> pk_type:long_term_key_type -> tr:trace ->
+  Lemma
+  (ensures (
+    let (opt_private_key, tr_out) = compute_public_key prin sess_id pk_type tr in
+    tr_out == tr
+  ))
+  [SMTPat (compute_public_key prin sess_id pk_type tr);]
+let compute_public_key_same_trace prin sess_id pk_type tr =
+  reveal_opaque (`%compute_public_key) (compute_public_key)
+
+
 val compute_public_key_invariant:
   {|protocol_invariants|} ->
   prin:principal -> sess_id:state_id -> pk_type:long_term_key_type -> tr:trace ->
@@ -206,12 +229,10 @@ val compute_public_key_invariant:
   )
   (ensures (
     let (opt_private_key, tr_out) = compute_public_key prin sess_id pk_type tr in
-    tr_out == tr /\ (
-      match opt_private_key with
-      | None -> True
-      | Some private_key ->
+    match opt_private_key with
+    | None -> True
+    | Some private_key ->
         is_public_key_for tr private_key pk_type prin
-    )
   ))
   [SMTPat (compute_public_key prin sess_id pk_type tr);
    SMTPat (has_private_keys_invariant);
diff --git a/src/lib/state/DY.Lib.State.Tagged.fst b/src/lib/state/DY.Lib.State.Tagged.fst
index 814c618..652cf76 100644
--- a/src/lib/state/DY.Lib.State.Tagged.fst
+++ b/src/lib/state/DY.Lib.State.Tagged.fst
@@ -264,6 +264,19 @@ let get_tagged_state the_tag prin sess_id =
       if tag = the_tag then return (Some content)
       else return None
 
+val set_tagged_state_state_was_set:
+  tag:string -> 
+  prin:principal -> sess_id:state_id -> content:bytes -> tr:trace ->
+  Lemma
+  (ensures (
+    let ((), tr_out) = set_tagged_state tag prin sess_id content tr in
+    tagged_state_was_set tr_out tag prin sess_id content
+  ))
+  [SMTPat (set_tagged_state tag prin sess_id content tr);]
+let set_tagged_state_state_was_set tag prin sess_id content tr =
+  reveal_opaque (`%set_tagged_state) (set_tagged_state);
+  reveal_opaque (`%tagged_state_was_set) (tagged_state_was_set)
+
 val set_tagged_state_invariant:
   {|protocol_invariants|} ->
   tag:string -> spred:local_bytes_state_predicate tag ->
@@ -276,8 +289,7 @@ val set_tagged_state_invariant:
   )
   (ensures (
     let ((), tr_out) = set_tagged_state tag prin sess_id content tr in
-    trace_invariant tr_out /\
-    tagged_state_was_set tr_out tag prin sess_id content
+    trace_invariant tr_out
   ))
   [SMTPat (set_tagged_state tag prin sess_id content tr);
    SMTPat (trace_invariant tr);
@@ -285,42 +297,43 @@ val set_tagged_state_invariant:
 let set_tagged_state_invariant #invs tag spred prin sess_id content tr =
   reveal_opaque (`%has_local_bytes_state_predicate) (has_local_bytes_state_predicate);
   reveal_opaque (`%set_tagged_state) (set_tagged_state);
-  reveal_opaque (`%tagged_state_was_set) (tagged_state_was_set);
   let full_content = {tag; content;} in
-  parse_serialize_inv_lemma #bytes tagged_state full_content;
   local_eq_global_lemma split_local_bytes_state_predicate_params state_pred.pred tag spred (tr, prin, sess_id, serialize _ full_content) tag (tr, prin, sess_id, content)
 
-val get_tagged_state_invariant:
-  {|protocol_invariants|} ->
-  tag:string -> spred:local_bytes_state_predicate tag ->
+val get_tagged_state_same_trace:
+  tag:string -> 
   prin:principal -> sess_id:state_id -> tr:trace ->
   Lemma
-  (requires
-    trace_invariant tr /\
-    has_local_bytes_state_predicate (|tag, spred|)
-  )
   (ensures (
     let (opt_content, tr_out) = get_tagged_state tag prin sess_id tr in
-    tr == tr_out /\ (
-      match opt_content with
-      | None -> True
-      | Some content -> (
-        spred.pred tr prin sess_id content
-      )
-    )
+    tr == tr_out 
   ))
-  [SMTPat (get_tagged_state tag prin sess_id tr);
-   SMTPat (trace_invariant tr);
-   SMTPat (has_local_bytes_state_predicate (|tag, spred|))]
-let get_tagged_state_invariant #invs tag spred prin sess_id tr =
-  reveal_opaque (`%has_local_bytes_state_predicate) (has_local_bytes_state_predicate);
+  [SMTPat (get_tagged_state tag prin sess_id tr);]
+let get_tagged_state_same_trace tag prin sess_id tr =
+  reveal_opaque (`%get_tagged_state) (get_tagged_state)
+
+
+val get_tagged_state_state_was_set:
+  tag:string -> 
+  prin:principal -> sess_id:state_id -> tr:trace ->
+  Lemma
+  (ensures (
+    let (opt_content, tr_out) = get_tagged_state tag prin sess_id tr in
+    match opt_content with
+    | None -> True
+    | Some content ->
+        tagged_state_was_set tr tag prin sess_id content
+  ))
+  [SMTPat (get_tagged_state tag prin sess_id tr)]
+let get_tagged_state_state_was_set tag prin sess_id tr =
   reveal_opaque (`%get_tagged_state) (get_tagged_state);
-  let (opt_content, tr_out) = get_tagged_state tag prin sess_id tr in
-  match opt_content with
-  | None -> ()
-  | Some content ->
-    let (Some full_content_bytes, tr) = get_state prin sess_id tr in
-    local_eq_global_lemma split_local_bytes_state_predicate_params state_pred.pred tag spred (tr, prin, sess_id, full_content_bytes) tag (tr, prin, sess_id, content)
+  reveal_opaque (`%tagged_state_was_set) (tagged_state_was_set);
+  match get_tagged_state tag prin sess_id tr with
+  | (None, _) -> ()
+  | (Some _, _) -> (
+    let (Some full_cont_bytes, _) = get_state prin sess_id tr in
+    serialize_parse_inv_lemma #bytes tagged_state full_cont_bytes    
+  )
 
 (*** Theorem ***)
 
diff --git a/src/lib/state/DY.Lib.State.Typed.fst b/src/lib/state/DY.Lib.State.Typed.fst
index 1a2df60..cb16b45 100644
--- a/src/lib/state/DY.Lib.State.Typed.fst
+++ b/src/lib/state/DY.Lib.State.Typed.fst
@@ -173,6 +173,20 @@ let get_state #a #ls prin sess_id =
   | None -> return None
   | Some content -> return (Some content)
 
+
+val set_state_state_was_set:
+  #a:Type -> {|ls:local_state a|} ->
+  prin:principal -> sess_id:state_id -> content:a -> tr:trace ->
+  Lemma
+  (ensures (
+    let ((), tr_out) = set_state prin sess_id content tr in
+    state_was_set tr_out prin sess_id content
+  ))
+  [SMTPat (set_state #a #ls prin sess_id content tr);]
+let set_state_state_was_set #a #ls  prin sess_id content tr =
+  reveal_opaque (`%set_state) (set_state #a);
+  reveal_opaque (`%state_was_set) (state_was_set #a #ls)
+
 val set_state_invariant:
   #a:Type -> {|local_state a|} ->
   {|protocol_invariants|} ->
@@ -186,42 +200,49 @@ val set_state_invariant:
   )
   (ensures (
     let ((), tr_out) = set_state prin sess_id content tr in
-    trace_invariant tr_out /\
-    state_was_set tr_out prin sess_id content
+    trace_invariant tr_out
   ))
   [SMTPat (set_state prin sess_id content tr);
    SMTPat (trace_invariant tr);
    SMTPat (has_local_state_predicate spred)]
 let set_state_invariant #a #ls #invs spred prin sess_id content tr =
   reveal_opaque (`%set_state) (set_state #a);
-  reveal_opaque (`%state_was_set) (state_was_set #a);
   parse_serialize_inv_lemma #bytes a content
 
-val get_state_invariant:
-  #a:Type -> {|local_state a|} ->
-  {|protocol_invariants|} ->
-  spred:local_state_predicate a ->
+
+val get_state_same_trace:
+  #a:Type -> {|ls:local_state a|} ->
   prin:principal -> sess_id:state_id -> tr:trace ->
   Lemma
-  (requires
-    trace_invariant tr /\
-    has_local_state_predicate spred
-  )
   (ensures (
-    let (opt_content, tr_out) = get_state prin sess_id tr in
-    tr == tr_out /\ (
-      match opt_content with
-      | None -> True
-      | Some content -> (
-        spred.pred tr prin sess_id content
-      )
-    )
+    let (opt_content, tr_out) = get_state #a prin sess_id tr in
+    tr == tr_out
   ))
-  [SMTPat (get_state #a prin sess_id tr);
-   SMTPat (trace_invariant tr);
-   SMTPat (has_local_state_predicate spred)]
-let get_state_invariant #a #ls #invs spred prin sess_id tr =
-  reveal_opaque (`%get_state) (get_state #a)
+  [SMTPat (get_state #a #ls prin sess_id tr);]
+let get_state_same_trace #a #ls prin sess_id tr =
+  reveal_opaque (`%get_state) (get_state #a #ls)
+
+
+val get_state_state_was_set:
+  #a:Type -> {|ls:local_state a|} ->
+  prin:principal -> sess_id:state_id -> tr:trace ->
+  Lemma
+  (ensures (
+    let (opt_content, tr_out) = get_state #a #ls prin sess_id tr in
+    match opt_content with
+    | None -> True
+    | Some content -> 
+        state_was_set tr prin sess_id content
+  ))
+  [SMTPat (get_state #a #ls prin sess_id tr)]
+let get_state_state_was_set #a #ls prin sess_id tr =
+  reveal_opaque (`%get_state) (get_state #a #ls);
+  reveal_opaque (`%state_was_set) (state_was_set #a #ls);
+  match get_state #a #ls prin sess_id tr with
+  | (None, _) -> ()
+  | (Some _, _) ->
+      let (Some cont, _) = get_tagged_state ls.tag prin sess_id tr in
+      serialize_parse_inv_lemma a cont
 
 val state_was_set_implies_pred:
   #a:Type -> {|local_state a|} ->