diff --git a/meta.yml b/meta.yml
index 96a0acb..44c898b 100644
--- a/meta.yml
+++ b/meta.yml
@@ -10,7 +10,7 @@ authors:
   - name: "Will Thomas"
     email: "30wthomas@ku.edu"
 opam-file-maintainer: "30wthomas@ku.edu" # Need a strong default here or we will accidentally email a Coq developer
-opam-file-version: "0.2.0"
+opam-file-version: "0.6.0"
 
 ######################################################
 # NOTE: Optional Extra Info
@@ -26,17 +26,17 @@ dependencies:
   - description: "[RocqCandy](https://github.com/ku-sldg/rocq-candy)"
     opam:
       name: "rocq-candy"
-      version: '{ >= "0.2.1" }'
+      version: '{ >= "0.6.0" }'
       lib_name: "RocqCandy"
   - description: "[Copland Spec](https://github.com/ku-sldg/copland-spec)"
     opam:
       name: "rocq-copland-spec"
-      version: '{ >= "0.1.1" }'
+      version: '{ >= "0.6.0" }'
       lib_name: "CoplandSpec"
   - description: "[CoplandManifestTools](https://github.com/ku-sldg/copland-manifest-tools)"
     opam:
       name: "rocq-copland-manifest-tools"
-      version: '{ >= "0.2.4" }'
+      version: '{ >= "0.6.0" }'
       lib_name: "CoplandManifestTools"
   - description: "[EasyBakeCakeML](https://github.com/Durbatuluk1701/EasyBakeCakeML)"
     opam:
diff --git a/rocq-cvm.opam b/rocq-cvm.opam
index 9730279..6edc00d 100644
--- a/rocq-cvm.opam
+++ b/rocq-cvm.opam
@@ -3,7 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "30wthomas@ku.edu"
-version: "0.2.0"
+version: "0.6.0"
 
 homepage: "https://github.com/ku-sldg/cvm"
 dev-repo: "git+https://github.com/ku-sldg/cvm.git"
@@ -19,9 +19,9 @@ depends: [
   "ocaml" { >= "4.12~" }
   "dune" {>= "3.17"}
   "coq"  { = "9.0.1" }
-  "rocq-candy" { >= "0.2.1" }
-  "rocq-copland-spec" { >= "0.1.1" }
-  "rocq-copland-manifest-tools" { >= "0.2.4" }
+  "rocq-candy" { >= "0.6.0" }
+  "rocq-copland-spec" { >= "0.6.0" }
+  "rocq-copland-manifest-tools" { >= "0.6.0" }
   "rocq-EasyBakeCakeML" { >= "0.5.0" }
   "bake" { >= "1.4.0" }
   "rocq-logging" { >= "0.1.2" }
diff --git a/theories/Impl.v b/theories/Impl.v
index 80d49ad..6be427c 100644
--- a/theories/Impl.v
+++ b/theories/Impl.v
@@ -11,6 +11,20 @@ From RocqCandy Require Import All.
 From CoplandSpec Require Import Term_Defs.
 From CVM Require Import Monad.
 
+Definition proc_ev_path_left_ev (ep : ev_path) e : Evidence :=
+  match ep with
+  | left_path => e
+  | right_path => mt_evc
+  | both_paths => e
+  end.
+
+Definition proc_ev_path_right_ev (ep : ev_path) e : Evidence :=
+  match ep with
+  | left_path => mt_evc
+  | right_path => e
+  | both_paths => e
+  end.
+
 (** Monadic CVM implementation (top-level) *)
 Fixpoint build_cvm (e : Evidence) (t: Term) : CVM Evidence :=
   match t with
@@ -20,18 +34,18 @@ Fixpoint build_cvm (e : Evidence) (t: Term) : CVM Evidence :=
     e1 <- build_cvm e t1 ;;cvm
     build_cvm e1 t2
 
-  | bseq s t1 t2 =>
+  | bseq ep t1 t2 =>
     split_ev ;;cvm
-    e1r <- build_cvm (splitEv_l s e) t1 ;;cvm
-    e2r <- build_cvm (splitEv_r s e) t2 ;;cvm
+    e1r <- build_cvm (proc_ev_path_left_ev ep e) t1 ;;cvm
+    e2r <- build_cvm (proc_ev_path_right_ev ep e) t2 ;;cvm
     join_seq e1r e2r
 
-  | bpar s t1 t2 =>
+  | bpar ep t1 t2 =>
     split_ev ;;cvm
     (* We will make the LOC = event_id for start of thread *)
     (* start a parallel thread working on the evidence split for t2 *)
-    loc <- start_par_thread (splitEv_r s e) t2 ;;cvm
-    e1r <- build_cvm (splitEv_l s e) t1 ;;cvm
-    e2r <- wait_par_thread loc (splitEv_r s e) t2 ;;cvm
+    loc <- start_par_thread e t2 ;;cvm
+    e1r <- build_cvm (proc_ev_path_left_ev ep e) t1 ;;cvm
+    e2r <- wait_par_thread loc (proc_ev_path_right_ev ep e) t2 ;;cvm
     join_seq e1r e2r
   end.
diff --git a/theories/Monad.v b/theories/Monad.v
index 3a027e1..e2fee62 100644
--- a/theories/Monad.v
+++ b/theories/Monad.v
@@ -112,40 +112,43 @@ Hint Unfold get_asp_dual : cvm.
 
 Definition bundle_asp `{DecEq nat, DecEq ASP_ID} (p:Plc) (rwev : RawEv) 
     (cur_ev : Evidence) (ps:ASP_PARAMS) : CVM Evidence :=
-  let '(asp_paramsC asp_id args targ_plc targ) := ps in
-  '(ev_arrow fwd in_sig out_sig) <- get_asp_type asp_id ;;cvm
-  match out_sig with
-  | (OutN n) =>
+  let '(asp_paramsC asp_id args) := ps in
+  '(ev_arrow fwd attrs) <- get_asp_type asp_id ;;cvm
+  match fwd with
+  | EXTEND (exist _ n nlt) _ =>
     match (dec_eq (List.length rwev) n) with
     | left _ => 
-      match fwd with
+(* The semantics for an "EXTEND" asp are it APPENDS all incoming evidence to the
+current CVM evidence bundle *)
+      match cur_ev with
+      | evc bits et => CVM_ret (evc (rwev ++ bits) (asp_evt p ps et))
+      end
+    | right _ => 
+      (* we are not the right size, so we fail *)
+      CVM_fail (dispatch_error (Runtime errStr_raw_EvidenceT_too_long))
+    end
+  | REPLACE (exist _ n nlt) =>
 (* The semantics for a "REPLACE" asp are it CONSUMES all incoming evidence,
 then returns a new collection of evidence that will REPLACE the CVMs current 
 Evidence *)
-      | REPLACE => CVM_ret (evc rwev (asp_evt p ps (get_et cur_ev)))
+    match (dec_eq (List.length rwev) n) with
+    | left _ => CVM_ret (evc rwev (asp_evt p ps (get_et cur_ev)))
+    | right _ => 
+      (* we are not the right size, so we fail *)
+      CVM_fail (dispatch_error (Runtime errStr_raw_EvidenceT_too_long))
+    end
 (* The semantics for a "WRAP" asp are the exact same as "REPLACE" for the 
 attestation and bundling side of the CVM. Wraps main distinction lies in the
 fact that its is a GUARANTEE, that the dual appraisal ASP is actually an
 inverse, thus allowing WRAPPED evidence to be recovered via appraisal *)
-      | WRAP => CVM_ret (evc rwev (asp_evt p ps (get_et cur_ev)))
-      | UNWRAP => CVM_fail (dispatch_error (Runtime err_str_unwrap_must_have_outwrap))
-(* The semantics for an "EXTEND" asp are it APPENDS all incoming evidence to the
-current CVM evidence bundle *)
-      | EXTEND =>
-        match cur_ev with
-        | evc bits et => CVM_ret (evc (rwev ++ bits) (asp_evt p ps et))
-        end
-      end
+  | WRAP (exist _ n nlt) =>
+    match (dec_eq (List.length rwev) n) with
+    | left _ => CVM_ret (evc rwev (asp_evt p ps (get_et cur_ev))) 
     | right _ => 
       (* we are not the right size, so we fail *)
       CVM_fail (dispatch_error (Runtime errStr_raw_EvidenceT_too_long))
     end
-  | OutUnwrap =>
-    match fwd with
-    | WRAP => CVM_fail (dispatch_error (Runtime err_str_only_unwrap_can_be_outwrap))
-    | REPLACE => CVM_fail (dispatch_error (Runtime err_str_only_unwrap_can_be_outwrap))
-    | EXTEND => CVM_fail (dispatch_error (Runtime err_str_only_unwrap_can_be_outwrap))
-    | UNWRAP => 
+  | UNWRAP =>
       sc <- get_config ;;cvm
       let G := (session_context sc) in
       let '(evc bits et) := cur_ev in
@@ -159,7 +162,7 @@ current CVM evidence bundle *)
       end
       (* match r with
       | asp_evt p' (asp_paramsC wrap_id _ _ _) et' =>
-        '(ev_arrow fwd _ _) <- get_asp_type wrap_id ;;cvm
+        '(ev_arrow fwd _) <- get_asp_type wrap_id ;;cvm
         match fwd with
         | WRAP =>
           (* we are an UNWRAP or a WRAP, so new size is the sizer of et' *)
@@ -175,7 +178,6 @@ current CVM evidence bundle *)
         end
       | _ => fail (dispatch_error (Runtime err_str_unwrap_only_wrap))
       end *)
-    end
   end.
 Hint Unfold bundle_asp : cvm.
 
@@ -210,14 +212,14 @@ Fixpoint invoke_APPR' `{DecEq ASP_ID} (r : RawEv) (et : EvidenceT) (out_evt : Ev
   | mt_evt => CVM_ret mt_evc 
   | nonce_evt n' => invoke_ASP (evc r out_evt) check_nonce_params
   | asp_evt p' par et' =>
-    let '(asp_paramsC asp_id args targ_plc targ) := par in
+    let '(asp_paramsC asp_id args ) := par in
     appr_asp_id <- get_asp_dual asp_id ;;cvm
-    let dual_par := asp_paramsC appr_asp_id args targ_plc targ in
-    '(ev_arrow fwd in_sig out_sig) <- get_asp_type asp_id ;;cvm
+    let dual_par := asp_paramsC appr_asp_id args in
+    '(ev_arrow fwd attrs) <- get_asp_type asp_id ;;cvm
     match fwd with
-    | REPLACE => (* Only do the dual ASP *)
+    | REPLACE n => (* Only do the dual ASP *)
       invoke_ASP (evc r out_evt) dual_par
-    | WRAP =>
+    | WRAP n =>
       (* first do the dual ASP to unwrap *)
       (* NOTE: Do we need to be checking that appr_asp_id is an UNWRAP here? *)
       '(evc r'' et'') <- invoke_ASP (evc r out_evt) dual_par ;;cvm
@@ -233,35 +235,26 @@ Fixpoint invoke_APPR' `{DecEq ASP_ID} (r : RawEv) (et : EvidenceT) (out_evt : Ev
     | UNWRAP =>
       (* to appraise an UNWRAP is to appraise whatever is below 
       the UNWRAP and WRAP *)
-      match out_sig with
-      | OutN _ => CVM_fail (dispatch_error (Runtime err_str_unwrap_must_have_outwrap)) 
-      | OutUnwrap =>
-        e <- hoist_result (apply_to_evidence_below G (fun e => invoke_APPR' r e out_evt) [Trail_UNWRAP asp_id] et') ;;cvm
-        e 
+      e <- hoist_result (apply_to_evidence_below G (fun e => invoke_APPR' r e out_evt) [Trail_UNWRAP asp_id] et') ;;cvm
+      e 
         (* e <- hoist_result (
           apply_to_asp_under_wrap G asp_id (fun e => invoke_APPR' r e out_evt) et'
         ) ;;
         e *)
-      end
-
-    | EXTEND =>
-      match out_sig with
-      | OutUnwrap => CVM_fail (dispatch_error (Runtime err_str_extend_must_have_outn))
-      | (OutN n) =>
-        (* first we split, left for the appr of extended part, right for rest *)
-        split_ev ;;cvm
-        '(_, r_ev) <- (hoist_result (peel_n_rawev n r)) ;;cvm
-
-        (* on left we do the dual of EXTEND *)
-        ev1 <- invoke_ASP (evc r out_evt) dual_par ;;cvm
-
-        (* now on right, we work only on the remaining evidence *)
-        (* our new evidence is e' *)
-        (* now we do the recursive call *)
-        ev2 <- invoke_APPR' r_ev et' et' ;;cvm
-        (* now join *)
-        join_seq ev1 ev2 
-      end
+    | EXTEND (exist _ n nlt) _ =>
+      (* first we split, left for the appr of extended part, right for rest *)
+      split_ev ;;cvm
+      '(_, r_ev) <- (hoist_result (peel_n_rawev n r)) ;;cvm
+
+      (* on left we do the dual of EXTEND *)
+      ev1 <- invoke_ASP (evc r out_evt) dual_par ;;cvm
+
+      (* now on right, we work only on the remaining evidence *)
+      (* our new evidence is e' *)
+      (* now we do the recursive call *)
+      ev2 <- invoke_APPR' r_ev et' et' ;;cvm
+      (* now join *)
+      join_seq ev1 ev2 
       (* ev' <- invoke_ASP (asp_paramsC appr_asp_id args targ_plc targ) ;;cvm
       put_ev ev' *)
     end
@@ -364,8 +357,8 @@ Hint Unfold get_cvm_policy : cvm.
 
 (* Remote communication primitives *)
 
-Definition do_remote (sc : Session_Config) (pTo: Plc) (e : Evidence) (t:Term) 
-    : Result Evidence CVM_Error := 
+Definition do_remote (sc : Session_Config) (pTo: Plc) (e : Evidence) (tm:Term) 
+    : Result Evidence CVM_Error :=
   (* There is assuredly a better way to do it than this *)
   let '(mkAtt_Sess my_plc plc_map pk_map G) := (session_config_decompiler sc) in
   (* We need  to update the Att Session to tell the next plc how
@@ -374,7 +367,7 @@ Definition do_remote (sc : Session_Config) (pTo: Plc) (e : Evidence) (t:Term)
   let new_att_sess := (mkAtt_Sess pTo plc_map pk_map G) in
   match (plc_map ![ pTo ]) with 
   | Some IP_Port => 
-      let remote_req := (mkPRReq new_att_sess my_plc e t) in
+      let remote_req := (mkPRReq new_att_sess my_plc e tm) in
       let js_req := to_JSON remote_req in
       let resp_res := make_JSON_Network_Request IP_Port js_req in
       match resp_res with
@@ -392,7 +385,7 @@ Definition do_remote (sc : Session_Config) (pTo: Plc) (e : Evidence) (t:Term)
   | None => err (dispatch_error Unavailable)
   end.
 (* We make this Opaque because we want to hide its implementation details: we axiomatically manage remote calls instead *)
-Opaque do_remote.
+Global Opaque do_remote.
 
 Definition doRemote_session' (pTo:Plc) (e:Evidence) (t:Term) 
     : CVM Evidence := 
diff --git a/theories/Session_Config_Compiler.v b/theories/Session_Config_Compiler.v
index e88700d..5240225 100644
--- a/theories/Session_Config_Compiler.v
+++ b/theories/Session_Config_Compiler.v
@@ -4,7 +4,7 @@ From CoplandManifestTools Require Import Manifest.
 From CVM Require Import IO_Utils AM_Manager.
 
 Definition generate_ASP_dispatcher' (am : Manifest) (ats : Attestation_Session) (aspBin : FS_Location) (par : ASP_PARAMS) (rawEv : RawEv) : Result RawEv DispatcherErrors :=
-  let (aspid, args, targ_plc, targ) := par in
+  let (aspid, args) := par in
   let asps := am.(asps) in
   let asp_map := am.(ASP_Mapping) in
     (* check is the ASPID is available *) 
@@ -17,7 +17,7 @@ Definition generate_ASP_dispatcher' (am : Manifest) (ats : Attestation_Session)
         | None => (aspid_to_fs_location aspid)
         end 
       in
-        let asp_req := (mkASPRReq aspid args targ_plc targ rawEv) in
+        let asp_req := (mkASPRReq aspid args rawEv) in
         let js_req := to_JSON asp_req in
         let resp_res := make_JSON_FS_Location_Request aspBin conc_asp_loc js_req in
         match resp_res with
diff --git a/theories/Verification.v b/theories/Verification.v
index ce32007..93c7ab6 100644
--- a/theories/Verification.v
+++ b/theories/Verification.v
@@ -23,14 +23,14 @@ Lemma peel_n_rawev_result_spec : forall n ls ls1 ls2,
   peel_n_rawev n ls = res (ls1, ls2) ->
   ls = ls1 ++ ls2 /\ length ls1 = n.
 Proof.
-  induction n; ff u, a.
+  induction n; ff with u, a.
 Qed.
 
 Lemma peel_n_none_spec : forall n ls e,
   peel_n_rawev n ls = err e ->
   length ls < n.
 Proof.
-  induction n; ff u, a, l.
+  induction n; ff with u, a, l.
 Qed.
 
 Lemma invoke_APPR_deterministic : forall G e sc st1 st2 st1' st2' res1 res2 r oe,
@@ -44,7 +44,7 @@ Proof.
   induction e using (Evidence_subterm_path_Ind_special G);
   simpl in *; intros;
   try (ux cvm (); intuition; repeat find_injection; eauto; fail).
-  - ff (ux cvm).
+  - ff with (ux cvm ()).
   - ux cvm ();
     target_break_match H3; ff;
     try (Control.enter (fun () =>
@@ -63,7 +63,8 @@ Proof.
     repeat find_rewrite;
     subst; try (simple congruence 3);
     eauto.
-    ateb_unpack H9; ff a.
+    unpack_atebs.
+    find_eapply_lem_hyp H0; ff.
   - cvm_monad_unfold;
     target_break_match H2;
     repeat find_injection;
@@ -76,13 +77,15 @@ Proof.
     repeat find_rewrite;
     subst; try (simple congruence 3);
     eauto;
-    unpack_atebs; ff a.
+    unpack_atebs;
+    find_eapply_lem_hyp H; ff.
   - cvm_monad_unfold;
     target_break_match H2;
     repeat find_injection;
     repeat find_rewrite;
     subst; try (simple congruence 3);
-    eauto; unpack_atebs; ff a.
+    eauto; unpack_atebs. 
+    find_eapply_lem_hyp H; ff.
   - cvm_monad_unfold;
     target_break_match H1;
     repeat find_injection;
@@ -132,7 +135,7 @@ Proof.
     subst; try (simple congruence 3);
     eauto;
     try (target_break_match H3).
-    unpack_atebs; ff a.
+    unpack_atebs; ff with (a).
   - target_break_match H2;
     repeat find_injection;
     repeat find_rewrite;
@@ -154,14 +157,14 @@ Proof.
     subst; try (simple congruence 3);
     eauto;
     try (target_break_match H3);
-    unpack_atebs; ff a.
+    unpack_atebs; ff with (a).
   - target_break_match H2;
     repeat find_injection;
     repeat find_rewrite;
     subst; try (simple congruence 3);
     eauto;
     try (target_break_match H3);
-    unpack_atebs; ff a.
+    unpack_atebs; ff with (a).
   - target_break_match H0;
     repeat find_injection;
     repeat find_rewrite;
@@ -185,7 +188,7 @@ Lemma cvm_deterministic :  forall t e sc st1 st2 r1 r2 st1' st2',
   build_cvm e t sc st2 = (r2, st2') ->
   (r1 = r2) /\ (st_evid st1' = st_evid st2').
 Proof.
-  induction t; simpl in *; cvm_monad_unfold; ff;
+  induction t; ff with (cvm_monad_unfold);
   repeat (match! goal with
   | [ u : unit |- _ ] => 
     let u := Control.hyp u in
@@ -198,7 +201,7 @@ Proof.
       eapply $ihv in $h1 > [ | | eapply $h2v ]; ff;
       try (clear $ih $h2)
   end);
-  solve [ eapply invoke_APPR_deterministic; ff ].
+  try (  solve [ eapply invoke_APPR_deterministic; ff ]).
 Qed.
 
 Lemma appr_events'_errs_deterministic : forall G p e e' i1 e1,
@@ -207,13 +210,13 @@ Lemma appr_events'_errs_deterministic : forall G p e e' i1 e1,
 Proof.
   intros G.
   induction e using (Evidence_subterm_path_Ind_special G);
-  intros; simpl in *; ff u, a;
+  intros; simpl in *; ff with u, (a);
   try (find_eapply_lem_hyp IHe; ff; fail);
   try (find_eapply_lem_hyp IHe1; ff);
   try (find_eapply_lem_hyp IHe2; ff);
   try (ateb_errs_same; eauto; fail);
   try (ateb_diff);
-  try (ateb_same); ff a.
+  try (ateb_same); ff with (a).
 Qed.
 
 Lemma asp_events_errs_deterministic : forall G t p e i1 i2 e1 e2,
@@ -231,7 +234,7 @@ Lemma events_fix_errs_deterministic : forall G t p e i1 i2 e1 e2,
   events_fix G p e t i2 = err e2 ->
   False.
 Proof.
-  induction t; ff u, a;
+  induction t; ff with u, a;
   eapply asp_events_errs_deterministic; eauto.
 Qed.
 
@@ -240,7 +243,7 @@ Lemma events_fix_only_one_error : forall G t p e i1 i2 e1 e2,
   events_fix G p e t i2 = err e2 ->
   e1 = e2.
 Proof.
-  induction t; ff u, a;
+  induction t; ff with u, a;
   try (match! goal with
   | [ h1 : events_fix _ _ _ ?_t _ = res _,
       h2 : events_fix _ _ _ ?_t _ = err _ |- _ ] =>
@@ -292,11 +295,10 @@ Proof.
         eapply $ihv in $h1 > [ | eapply $h2v];
         clear $ih $h2; ff
     end)).
-  - ff; simpl in *; 
+  - ff; try (
     repeat (match! goal with
     | [ h : parallel_vm_thread _ _ _ _ = ?_res |- _ ] =>
-      eapply parallel_vm_thread_axiom in $h;
-      try reflexivity; break_exists
+      eapply parallel_vm_thread_axiom in $h; ff
     | [ h1 : build_cvm _ ?_t _ _ = _,
         h2 : build_cvm _ ?_t _ _ = _,
         ih : context[build_cvm _ ?_t _ _ = _ -> _] |- _ ] =>
@@ -311,7 +313,7 @@ Proof.
       let h2 := Control.hyp h2 in
       try (eapply events_fix_only_one_error in $h1; try (eapply $h2); ff; try eauto; fail);
       try (eapply events_fix_errs_deterministic in $h1; try (eapply $h2); ff; try eauto; fail)
-    end).
+    end); fail).
 Qed.
 
 Lemma invoke_APPR'_spans : forall G' et r e' sc c i st eo,
@@ -324,24 +326,24 @@ Lemma invoke_APPR'_spans : forall G' et r e' sc c i st eo,
 Proof.
   intros G'.
   induction et using (Evidence_subterm_path_Ind_special G');
-  ff u, (ux cvm), a;
+  ff with u, (ux cvm ()), a;
   repeat (match! goal with
   | [ h : invoke_APPR' _ ?_e _ _ _ = _,
       ih : context[invoke_APPR' _ ?_e _ _ _ = _ -> _] |- _ ] =>
     let ih := Control.hyp ih in
-    eapply $ih in $h; ff l;
+    eapply $ih in $h; ff with l;
     try lia
-  end); try (ateb_same); ff a.
+  end); try (ateb_same); ff with a.
 Qed.
 
 Inductive et_same_asps : EvidenceT -> EvidenceT -> Prop :=
 | et_same_asps_mt : et_same_asps mt_evt mt_evt
 | et_same_asps_nonce : forall n1 n2, et_same_asps (nonce_evt n1) (nonce_evt n2)
-| et_same_asps_asp : forall p1 p2 e1 e2 aid args1 args2 targp1 targp2 targ1 targ2,
+| et_same_asps_asp : forall p1 p2 e1 e2 aid args1 args2,
     et_same_asps e1 e2 ->
     et_same_asps 
-      (asp_evt p1 (asp_paramsC aid args1 targp1 targ1) e1) 
-      (asp_evt p2 (asp_paramsC aid args2 targp2 targ2) e2)
+      (asp_evt p1 (asp_paramsC aid args1) e1) 
+      (asp_evt p2 (asp_paramsC aid args2) e2)
 | et_same_asps_left : forall e1 e2,
     et_same_asps e1 e2 ->
     et_same_asps (left_evt e1) (left_evt e2)
@@ -364,6 +366,25 @@ Proof.
     destruct $a; eauto using et_same_asps
   end).
 Qed.
+Local Hint Resolve et_same_asps_refl : et_same_asps_db.
+
+Lemma et_same_asps_ev_path_left : forall e1 e2,
+  et_same_asps e1 e2 ->
+  forall ep,
+  et_same_asps (proc_ev_path_left ep e1) (proc_ev_path_left ep e2).
+Proof.
+  destruct ep; eauto using et_same_asps.
+Qed.
+Local Hint Resolve et_same_asps_ev_path_left : et_same_asps_db.
+
+Lemma et_same_asps_ev_path_right : forall e1 e2,
+  et_same_asps e1 e2 ->
+  forall ep,
+  et_same_asps (proc_ev_path_right ep e1) (proc_ev_path_right ep e2).
+Proof.
+  destruct ep; eauto using et_same_asps.
+Qed.
+Local Hint Resolve et_same_asps_ev_path_right : et_same_asps_db.
 
 Lemma et_same_asps_symm : forall e1 e2,
   et_same_asps e1 e2 -> et_same_asps e2 e1.
@@ -385,8 +406,6 @@ Proof.
   induction H; intros; simpl in *;
   try (invc H0; invc H1; eauto using et_same_asps; fail).
   - invc H0; invc H1; try congruence; eauto using et_same_asps.
-  - invc H0; invc H1; try congruence; eauto using et_same_asps.
-  - invc H0; invc H1; try congruence; eauto using et_same_asps.
   - invc H1; invc H2; try congruence; eauto using et_same_asps.
 Qed.
 Local Hint Resolve ev_subterm_path_et_same_asps : et_same_asps_db.
@@ -418,40 +437,40 @@ Proof.
   intros G.
   induction e1 using (Evidence_subterm_path_Ind_special G);
   intros; simpl in *; ff; eauto;
-  try (invc H; ff u, a; fail);
-  try (invc H1; ff u, a; fail).
-  - invc H1; ff u, a.
-    * unpack_atebs; ff a; eapply H0; ff a;
+  try (invc H; ff with u, a; fail);
+  try (invc H1; ff with u, a; fail).
+  - invc H1; ff with u, a.
+    * unpack_atebs; ff with a; eapply H0; ff with a;
       eapply ev_subterm_path_et_same_asps; ff.
-    * eapply et_same_asps_ateb_errs_only in Heqr; ff a; 
+    * find_eapply_lem_hyp @et_same_asps_ateb_errs_only; ff;
       eauto with et_same_asps_db.
-    * eapply et_same_asps_ateb_errs_only in Heqr0; ff a; 
+    * find_eapply_lem_hyp @et_same_asps_ateb_errs_only; ff;
       eauto with et_same_asps_db.
-    * f_equal; eapply et_same_asps_ateb_errs_det; ff a.
-  - invc H0; ff u, a.
-  - invc H0; ff u, a.
-    * unpack_atebs; ff a; eapply H; ff a;
+    * f_equal; eapply et_same_asps_ateb_errs_det; ff with a.
+  - invc H0; ff with u, a.
+  - invc H0; ff with u, a.
+    * unpack_atebs; ff with a; eapply H; ff with a;
       eapply ev_subterm_path_et_same_asps; ff.
-    * eapply et_same_asps_ateb_errs_only in Heqr; ff a; 
+    * find_eapply_lem_hyp @et_same_asps_ateb_errs_only; ff;
       eauto with et_same_asps_db.
-    * eapply et_same_asps_ateb_errs_only in Heqr0; ff a; 
+    * find_eapply_lem_hyp @et_same_asps_ateb_errs_only; ff;
       eauto with et_same_asps_db.
-    * f_equal; eapply et_same_asps_ateb_errs_det; ff a.
-  - invc H0; ff u, a.
-    * unpack_atebs; ff a; eapply H; ff a;
+    * f_equal; eapply et_same_asps_ateb_errs_det; ff.
+  - invc H0; ff with u, a.
+    * unpack_atebs; ff with a; eapply H; ff with a;
       eapply ev_subterm_path_et_same_asps; ff.
-    * eapply et_same_asps_ateb_errs_only in Heqr; ff a; 
+    * find_eapply_lem_hyp @et_same_asps_ateb_errs_only; ff;
       eauto with et_same_asps_db.
-    * eapply et_same_asps_ateb_errs_only in Heqr0; ff a; 
+    * find_eapply_lem_hyp @et_same_asps_ateb_errs_only; ff;
       eauto with et_same_asps_db.
-    * f_equal; eapply et_same_asps_ateb_errs_det; ff a.
+    * f_equal; eapply et_same_asps_ateb_errs_det; ff with a.
 Qed.
 Local Hint Resolve et_same_asps_impl_same_size : et_same_asps_db.
 
-Lemma et_same_asps_asp_dir : forall e1 e2 asp_id args1 args2 targ_plc1 targ_plc2 targ1 targ2 p1 p2 par1 par2,
+Lemma et_same_asps_asp_dir : forall e1 e2 asp_id args1 args2 p1 p2 par1 par2,
   et_same_asps e1 e2 ->
-  par1 = (asp_paramsC asp_id args1 targ_plc1 targ1) ->
-  par2 = (asp_paramsC asp_id args2 targ_plc2 targ2) ->
+  par1 = (asp_paramsC asp_id args1) ->
+  par2 = (asp_paramsC asp_id args2) ->
   et_same_asps (asp_evt p1 par1 e1) (asp_evt p2 par2 e2).
 Proof.
   intros.
@@ -466,7 +485,7 @@ Lemma equiv_EvidenceT_impl_et_size_same : forall G e1 e2,
   et_size G e1 = et_size G e2.
 Proof.
   intros.
-  unfold equiv_EvidenceT in *; ff u, a.
+  unfold equiv_EvidenceT in *; ff with u, a.
 Qed.
 
 Lemma et_same_asps_appr_procedure : forall G e1 e1' e2 e2' p1 p2 e1o e2o,
@@ -484,30 +503,25 @@ Proof.
   - inv H1; simpl in *; ff.
     * econstructor; eauto.
     * eapply IHe1 in H4; ff; econstructor; eauto.
-    * ff u, a.
+    * ff with u, a.
       econstructor; eauto.
       econstructor; eauto.
-  - inv H1; simpl in *; ff u, a;
-    ateb_unpack Heqr0;
-    ateb_unpack Heqr.
-    eapply H0 in Hf0; try (eapply Hf); ff.
+  - inv H1; simpl in *; ff with u, a;
+    unpack_atebs.
+    eapply H0 in Hf; try (eapply Hf0); ff.
     eapply ev_subterm_path_et_same_asps; ff.
   - inv H1; simpl in *; ff.
-  - inv H0; simpl in *; ff u, a.
-    ateb_unpack Heqr0;
-    ateb_unpack Heqr.
-    eapply H in Hf0; try (eapply Hf); ff.
+  - inv H0; simpl in *; ff with u, a.
+    unpack_atebs.
+    eapply H in Hf; try (eapply Hf0); ff.
     eapply ev_subterm_path_et_same_asps; ff.
-  - inv H0; simpl in *; ff u, a;
-    ateb_unpack Heqr0;
-    ateb_unpack Heqr.
-    eapply H in Hf0; try (eapply Hf); ff.
+  - inv H0; simpl in *; ff with u, a;
+    unpack_atebs.
+    eapply H in Hf; try (eapply Hf0); ff.
     eapply ev_subterm_path_et_same_asps; ff.
-  - inv H; simpl in *; ff u, a;
-    eapply IHe1_1 in Heqr; try (eapply Heqr1); eauto;
-    try (econstructor; eauto; fail).
-    eapply IHe1_2 in Heqr0; try (eapply Heqr2); eauto;
-    try (econstructor; eauto; fail).
+  - inv H; simpl in *; ff with u, a.
+    eapply IHe1_1 in Heq0; try (eapply Heq3); ff;
+    eauto using et_same_asps.
 Qed.
 Local Hint Resolve et_same_asps_appr_procedure : et_same_asps_db.
 
@@ -520,8 +534,8 @@ Proof.
   induction t; simpl in *; intuition; eauto.
   - destruct a; simpl in *; ff; eauto using et_same_asps.
     eapply et_same_asps_appr_procedure; eauto.
-  - ff u, a.
-  - ff u, a.
+  - ff with u, a.
+  - ff with u, a.
     repeat (match! goal with
     | [ h1 : eval _ ?_p1 ?_e1 ?_t = res ?_e1',
         h2 : eval _ ?_p2 ?_e2 ?_t = res ?_e2',
@@ -530,11 +544,8 @@ Proof.
       let ih := Control.hyp ih in
       eapply $ih in $h2; try (eapply $h1v); 
       clear $h1
-    end);
-    try (econstructor; eauto; fail);
-    destruct s, s, s0; simpl in *; eauto;
-    econstructor.
-  - ff u, a.
+    end); ff; eauto with et_same_asps_db.
+  - ff with u, a.
     repeat (match! goal with
     | [ h1 : eval _ ?_p1 ?_e1 ?_t = res ?_e1',
         h2 : eval _ ?_p2 ?_e2 ?_t = res ?_e2',
@@ -543,10 +554,7 @@ Proof.
       let ih := Control.hyp ih in
       eapply $ih in $h2; try (eapply $h1v); 
       clear $h1
-    end);
-    try (econstructor; eauto; fail);
-    destruct s, s, s0; simpl in *; eauto;
-    econstructor.
+    end); ff; eauto with et_same_asps_db.
 Qed.
 Local Hint Resolve et_same_asps_eval_same_asps : et_same_asps_db.
 
@@ -576,20 +584,14 @@ Lemma et_same_asps_impl_appr_events_size_same : forall G e1 e2 n1 n2,
 Proof.
   intros G.
   induction e1 using (Evidence_subterm_path_Ind_special G);
-  intros; simpl in *; ff u, a;
+  intros; simpl in *; ff with u, a;
   try (invc H; ff; fail);
-  try (invc H1; ff u, a; fail).
-  - invc H1; ff u, a.
-    ateb_unpack Heqr; ateb_unpack Heqr0.
-    eapply H0; ff; eapply ev_subterm_path_et_same_asps; eauto.
-  - invc H0; ff u, a.
-    ateb_unpack Heqr; ateb_unpack Heqr0.
-    eapply H; ff; eapply ev_subterm_path_et_same_asps; eauto.
-  - invc H0; ff u, a.
-    ateb_unpack Heqr; ateb_unpack Heqr0.
-    eapply H; ff; eapply ev_subterm_path_et_same_asps; eauto.
-  - invc H; simpl in *; ff u, a.
-    eapply IHe1_1 in Heqr1; try reflexivity; subst; ff.
+  try (invc H1; ff with u, a; fail).
+  - invc H1; ff with u, a; unpack_atebs; ff with (eauto with et_same_asps_db).
+  - invc H0; ff with u, a; unpack_atebs; ff with (eauto with et_same_asps_db).
+  - invc H0; ff with u, a; unpack_atebs; ff with (eauto with et_same_asps_db).
+  - invc H; ff with u, a.
+    find_eapply_lem_hyp IHe1_1; try (reflexivity); ff.
 Qed.
 
 Lemma events_size_eval_res_irrel : forall G t1 t p1 p2 et e1 e2 n1 n2,
@@ -606,10 +608,10 @@ Proof.
   );
   clear H H0 et.
   generalizeEverythingElse t.
-  induction t; simpl in *; intuition; ff u, a;
+  induction t; simpl in *; intuition; ff with u, a;
   eauto with et_same_asps_db.
   - eapply et_same_asps_impl_appr_events_size_same; eauto.
-  - destruct s, s, s0; simpl in *; ff u, a;
+  - simpl in *; ff with u, a;
     repeat (match! goal with
     | [ h1 : events_size _ ?_p1 ?_e1 ?_t1 = _,
         h2 : events_size _ ?_p2 ?_e2 ?_t1 = _,
@@ -620,8 +622,8 @@ Proof.
       try (eapply et_same_asps_symm; eauto; fail);
       try (eapply et_same_asps_refl; eauto; fail);
       clear $h2; ff
-    end).
-  - destruct s, s, s0; simpl in *; ff u, a;
+    end); eauto with et_same_asps_db.
+  - simpl in *; ff with u, a;
     repeat (match! goal with
     | [ h1 : events_size _ ?_p1 ?_e1 ?_t1 = _,
         h2 : events_size _ ?_p2 ?_e2 ?_t1 = _,
@@ -632,7 +634,7 @@ Proof.
       try (eapply et_same_asps_symm; eauto; fail);
       try (eapply et_same_asps_refl; eauto; fail);
       clear $h2; ff
-    end).
+    end); eauto with et_same_asps_db.
 Qed.
 
 Lemma events_size_plc_irrel : forall G t et p1 p2 n1 n2,
@@ -640,7 +642,7 @@ Lemma events_size_plc_irrel : forall G t et p1 p2 n1 n2,
   events_size G p2 et t = res n2 ->
   n1 = n2.
 Proof.
-  induction t; simpl in *; intuition; ff u, a;
+  induction t; simpl in *; intuition; ff with u, a;
   repeat (match! goal with
   | [ h1 : events_size _ _ _ ?_t = _,
       h2 : events_size _ _ _ ?_t = _,
@@ -650,14 +652,17 @@ Proof.
     eapply $ih in $h1 > [ | eapply $h2v ];
     clear $h2; ff
   end); try lia.
-  - eapply events_size_eval_res_irrel in Heqr4; ff.
+  - eapply events_size_eval_res_irrel in Heq4; ff.
 Qed.
 
 Definition well_formed_context (G : GlobalContext) : Prop :=
-  (asp_types G) ![ sig_aspid ] = Some (ev_arrow EXTEND InAll (OutN 1)) /\
-  (asp_types G) ![ hsh_aspid ] = Some (ev_arrow REPLACE InAll (OutN 1)) /\
-  (asp_types G) ![ enc_aspid ] = Some (ev_arrow WRAP InAll (OutN 1)) /\
-  (asp_types G) ![ check_nonce_aspid ] = Some (ev_arrow EXTEND InAll (OutN 1)).
+  (asp_types G) ![ sig_aspid ] 
+    = Some (ev_arrow (EXTEND (exist _ 1 Nat.lt_0_1) InAll) []) /\
+  (asp_types G) ![ hsh_aspid ] 
+    = Some (ev_arrow (REPLACE (exist _ 1 Nat.lt_0_1)) []) /\
+  (asp_types G) ![ enc_aspid ] = Some (ev_arrow (WRAP (exist _ 1 Nat.lt_0_1)) []) /\
+  (asp_types G) ![ check_nonce_aspid ] 
+    = Some (ev_arrow (EXTEND (exist _ 1 Nat.lt_0_1) InAll) []).
 
 Lemma invoke_ASP_evidence : forall e par st sc e' st',
   invoke_ASP e par sc st = (res e', st') ->
@@ -675,28 +680,28 @@ Proof.
   intros G.
   induction et using (Evidence_subterm_path_Ind_special G);
   intuition; simpl in *.
-  - simpl in *; cvm_monad_unfold; ff.
+  - ff with (cvm_monad_unfold).
   - cvm_monad_unfold; ff; cvm_monad_unfold; ff.
-  - cvm_monad_unfold; ff; cvm_monad_unfold; ff u, a.
+  - cvm_monad_unfold; ff; cvm_monad_unfold; ff with u, a.
     cvm_monad_unfold; ff.
     * find_eapply_lem_hyp IHet; ff; simpl in *; ff.
     * find_eapply_lem_hyp IHet; ff; simpl in *; ff.
     * find_eapply_lem_hyp IHet; ff; simpl in *; ff.
     * find_eapply_lem_hyp IHet; ff; simpl in *; ff.
     * find_eapply_lem_hyp IHet; ff; simpl in *; ff.
-  - cvm_monad_unfold; ff; cvm_monad_unfold; ff u;
-    cvm_monad_unfold; ff u.
+  - cvm_monad_unfold; ff; cvm_monad_unfold; ff with u;
+    cvm_monad_unfold; ff with u.
     * ateb_same; find_eapply_lem_hyp H0; ff; ff.
-  - cvm_monad_unfold; ff; cvm_monad_unfold; ff u;
-    cvm_monad_unfold; ff u.
-  - cvm_monad_unfold; ff; cvm_monad_unfold; ff u;
-    cvm_monad_unfold; ff u;
+  - cvm_monad_unfold; ff; cvm_monad_unfold; ff with u;
+    cvm_monad_unfold; ff with u.
+  - cvm_monad_unfold; ff; cvm_monad_unfold; ff with u;
+    cvm_monad_unfold; ff with u;
     ateb_same; find_eapply_lem_hyp H; ff; ff.
-  - cvm_monad_unfold; ff; cvm_monad_unfold; ff u;
-    cvm_monad_unfold; ff u;
+  - cvm_monad_unfold; ff; cvm_monad_unfold; ff with u;
+    cvm_monad_unfold; ff with u;
     ateb_same; find_eapply_lem_hyp H; ff; ff.
-  - cvm_monad_unfold; ff; cvm_monad_unfold; ff u;
-    cvm_monad_unfold; ff u, a.
+  - cvm_monad_unfold; ff; cvm_monad_unfold; ff with u;
+    cvm_monad_unfold; ff with u, a.
     
     repeat (match! goal with
     | [ h1 : invoke_APPR' _ ?_e ?_o _ _ = _,
@@ -722,8 +727,7 @@ Proof.
   - cvm_monad_unfold; ff.
     find_eapply_lem_hyp do_remote_res_axiom; ff.
     find_eapply_lem_hyp IHt; ff.
-    erewrite H1 in *; ff.
-  - ff u, a; cvm_monad_unfold; ff;
+  - ff with u, a; cvm_monad_unfold; ff;
     try (match! goal with
     | [ h1 : build_cvm _ ?_t1 _ _ = _,
         h2 : build_cvm _ ?_t2 _ _ = _,
@@ -734,15 +738,14 @@ Proof.
       eapply $ih1 in $h1 as ?; ff;
       eapply $ih2 in $h2; ff
     end).
-  - ff u, a; cvm_monad_unfold; ff;
-    destruct s, s, s0; simpl in *;
-    eapply IHt1 in Heqp as ?; ff;
-    eapply IHt2 in Heqp0 as ?; simpl in *;
-    ff; find_higher_order_rewrite; eauto.
-  - ff u, a; cvm_monad_unfold; ff;
-    destruct s, s, s0; ff u, a;
-    find_eapply_lem_hyp parallel_vm_thread_axiom; eauto; ff u, a;
+  - ff with u, a; cvm_monad_unfold; ff.
+    destruct e;
+    find_eapply_lem_hyp IHt1; ff;
+    find_eapply_lem_hyp IHt2; ff.
+  - ff with u, a; cvm_monad_unfold; ff;
+    find_eapply_lem_hyp parallel_vm_thread_axiom; eauto; ff with u, a;
     try (unfold mt_evc in *; ff);
+    destruct e;
     find_eapply_lem_hyp IHt1; ff;
     find_eapply_lem_hyp IHt2; ff.
     Unshelve. eapply 0.
@@ -758,10 +761,10 @@ Proof.
   induction t; simpl in *; intuition.
   - cvm_monad_unfold; ff.
     find_eapply_lem_hyp invoke_APPR'_spans; ff. 
-  - cvm_monad_unfold; ff u; 
+  - cvm_monad_unfold; ff with u; 
     find_eapply_lem_hyp events_size_plc_irrel;
-    try (eapply Heqr0); ff l.
-  - cvm_monad_unfold; ff u.
+    try (eapply Heq5); ff with l.
+  - cvm_monad_unfold; ff with u.
 
     match! goal with
     | [ h : build_cvm _ ?_t _ _ = _,
@@ -773,42 +776,15 @@ Proof.
       try (eapply cvm_evidence_type in $h as ?; ff);
       clear $h $ih
     end.
-    destruct e; simpl in *; ff.
-    eapply IHt2 in H0 as ? > [ | | eapply Heqr1]; ff l.
-  - cvm_monad_unfold; ff u, a.
-    eapply IHt1 in Heqp > [ | eauto | destruct s, s, s0; ff ]; ff.
-    eapply IHt2 in Heqp0 > [ | eauto | destruct s, s, s0; ff ]; ff.
-    lia.
-  - ff u, a; cvm_monad_unfold; ff;
-    repeat find_rewrite;
-    eapply IHt1 in Heqp; try (eapply Heqr);
-    simpl in *; eauto; ff;
-    destruct s, s, s0; simpl in *; ff; try lia;
-    repeat find_rewrite; repeat find_injection; try lia;
-    unfold mt_evc in *; ff l.
-Qed.
-
-Lemma wf_Evidence_split_l : forall G e s,
-  wf_Evidence G e ->
-  wf_Evidence G (splitEv_l s e).
-Proof.
-  intros; invc H;
-  unfold splitEv_l; ff;
-  econstructor; simpl in *; auto.
-  Unshelve. eapply 0.
-Qed.
-Local Hint Resolve wf_Evidence_split_l : wf_Evidence.
-
-Lemma wf_Evidence_split_r : forall G e s,
-  wf_Evidence G e ->
-  wf_Evidence G (splitEv_r s e).
-Proof.
-  intros; invc H;
-  unfold splitEv_r; ff;
-  econstructor; simpl in *; auto.
-  Unshelve. eapply 0.
+    find_eapply_lem_hyp IHt2; ff with l.
+  - cvm_monad_unfold; ff with u, a.
+    destruct e;
+    find_eapply_lem_hyp IHt1; ff;
+    find_eapply_lem_hyp IHt2; ff with l.
+  - ff with u, a, (cvm_monad_unfold).
+    destruct e;
+    find_eapply_lem_hyp IHt1; ff with l.
 Qed.
-Local Hint Resolve wf_Evidence_split_r : wf_Evidence.
 
 Lemma wf_Evidence_split : forall G r1 r2 et1 et2,
   wf_Evidence G (evc r1 et1) ->
@@ -854,22 +830,22 @@ Lemma wf_Evidence_exists : forall G e n,
 Proof.
   intros G; induction e using (Evidence_subterm_path_Ind_special G); ff;
   try (exists (meta_machinery_pad_n n nil); econstructor; eauto;
-    ff u;
+    ff with u;
     rewrite meta_machinery_pad_n_size; ff; fail).
   - eexists; eapply wf_Evidence_mt_evc. 
   - exists [passed_bs]; econstructor; eauto.
 Qed.
 
-Lemma wf_Evidence_asp_unfold_more : forall G r p e n a a1 p0 t,
-  wf_Evidence G (evc r (asp_evt p (asp_paramsC a a1 p0 t) e)) ->
+Lemma wf_Evidence_asp_unfold_more : forall G r p e n a a1,
+  wf_Evidence G (evc r (asp_evt p (asp_paramsC a a1) e)) ->
   et_size G e = res n ->
-  forall sig n',
-  (asp_types G) ![ a ] = Some (ev_arrow EXTEND sig (OutN n')) ->
-  et_size G (asp_evt p (asp_paramsC a a1 p0 t) e) = res (n' + n).
+  forall sig n' n'lt attrs,
+  (asp_types G) ![ a ] = Some (ev_arrow (EXTEND (exist _ n' n'lt) sig) attrs) ->
+  et_size G (asp_evt p (asp_paramsC a a1) e) = res (n' + n).
 Proof.
   intros.
   prep_induction H.
-  induction H; ff u.
+  induction H; ff with u.
 Qed.
 
 Lemma wf_Evidence_split_unfold : forall G r e1 e2,
@@ -878,14 +854,14 @@ Lemma wf_Evidence_split_unfold : forall G r e1 e2,
 Proof.
   intros.
   prep_induction H;
-  induction H; ff u; 
-  split; eapply wf_Evidence_exists; ff.
+  induction H; ff with u;
+  eapply wf_Evidence_exists; ff.
 Qed.
 
-Lemma wf_Evidence_asp_unpack : forall G r p e a0 a1 p0 t,
-  wf_Evidence G (evc r (asp_evt p (asp_paramsC a0 a1 p0 t) e)) ->
-  forall in_sig n n',
-  (asp_types G) ![ a0 ] = Some (ev_arrow EXTEND in_sig (OutN n)) ->
+Lemma wf_Evidence_asp_unpack : forall G r p e a0 a1,
+  wf_Evidence G (evc r (asp_evt p (asp_paramsC a0 a1) e)) ->
+  forall in_sig n n' nlt attrs,
+  (asp_types G) ![ a0 ] = Some (ev_arrow (EXTEND (exist _ n nlt) in_sig) attrs) ->
   et_size G e = res n' ->
   List.length r = n + n'.
 Proof.
@@ -907,16 +883,16 @@ Proof.
     repeat (match! goal with
     | [ h : wf_Evidence _ _ |- _ ] => 
       invc $h; ff
-    end); try (econstructor; ff; repeat (rewrite length_app); ff u;
+    end); try (econstructor; ff; repeat (rewrite length_app); ff with u;
     try (ateb_diff); fail).
 
-  - simpl in *; ff u; cvm_monad_unfold; ff.
-    all: try (ff u;
+  - simpl in *; ff with u; cvm_monad_unfold; ff.
+    all: try (ff with u;
       repeat (match! goal with
       | [ h : wf_Evidence _ _ |- _ ] => invc $h; ff
       end);
-      ff u;
-      try (find_eapply_lem_hyp peel_n_rawev_result_spec; ff u);
+      ff with u;
+      try (find_eapply_lem_hyp peel_n_rawev_result_spec; ff with u);
       try (match! goal with
       | [ h : invoke_APPR' _ ?_t _ _ _ = _, 
           ih : context[invoke_APPR' _ ?_t _ _ _ = _ -> _] |- _ ] =>
@@ -924,60 +900,70 @@ Proof.
         eapply $ihv in $h > [ eauto | reflexivity | | ]; clear $ih
       end);
       econstructor; repeat (match! goal with
-      | [ h : wf_Evidence _ _ |- _ ] => invc $h; ff u
+      | [ h : wf_Evidence _ _ |- _ ] => invc $h; ff with u
       end);
-      repeat (rewrite length_app in *); ff u, l; try (f_equal); lia).
+      repeat (rewrite length_app in *); ff with u, l; try (f_equal); lia).
   - repeat (cvm_monad_unfold; ff).
-    ateb_unpack Heqr0; ff a.
+    unpack_atebs; ff with a.
     eapply H0 in H4; ff.
-    invc H2; simpl in *; u (); ff;
-    ateb_unpack Heqr0.
+    invc H2; ff with u; unpack_atebs.
     eapply Evidence_Subterm_path_same in Hesp;
     try (eapply Hesp0); subst.
     econstructor; ff.
   - repeat (cvm_monad_unfold; ff).
   - repeat (cvm_monad_unfold; ff).
-    ateb_unpack Heqr0; ff a;
+    unpack_atebs; ff with a;
     eapply H in H3; ff.
-    invc H1; simpl in *; u (); ff;
-    ateb_unpack Heqr0.
+    invc H1; ff with u; unpack_atebs.
     eapply Evidence_Subterm_path_same in Hesp;
     try (eapply Hesp0); subst.
     econstructor; ff.
   - repeat (cvm_monad_unfold; ff);
-    ateb_unpack Heqr0; ff a.
+    unpack_atebs; ff with a.
     eapply H in H3; ff.
-    invc H1; simpl in *; u (); ff;
-    ateb_unpack Heqr0.
+    invc H1; ff with u; unpack_atebs.
     eapply Evidence_Subterm_path_same in Hesp;
     try (eapply Hesp0); subst.
     econstructor; ff.
   - simpl in *; ff; cvm_monad_unfold; ff.
     repeat (find_eapply_lem_hyp peel_n_rawev_result_spec); ff;
     repeat (rewrite app_nil_r in *); ff.
-    eapply IHet1 in Heqp3; try reflexivity.
-    * eapply IHet2 in Heqp4; try reflexivity;
-      econstructor; repeat (rewrite length_app in *); ff;
-      u (); ff;
+    eapply IHet1 in Heq1; ff.
+    * eapply IHet2 in Heq6; ff;
+      econstructor; repeat (rewrite length_app in *); ff with u;
       repeat (match! goal with
       | [ h : wf_Evidence _ _ |- _ ] => invc $h; ff
-      end); ff u;
+      end); ff with u;
       repeat (rewrite length_app in *); ff;
       repeat (find_eapply_lem_hyp equiv_EvidenceT_impl_et_size_same); ff.
-    * econstructor; repeat (rewrite length_app in *); ff u;
+    * econstructor; repeat (rewrite length_app in *); ff with u;
       repeat (match! goal with
       | [ h : wf_Evidence _ _ |- _ ] => invc $h; ff
-      end); ff u;
+      end); ff with u;
       repeat (rewrite length_app in *); ff;
       repeat (find_eapply_lem_hyp equiv_EvidenceT_impl_et_size_same); ff.
-    * econstructor; repeat (rewrite length_app in *); ff u;
+    * econstructor; repeat (rewrite length_app in *); ff with u;
       repeat (match! goal with
       | [ h : wf_Evidence _ _ |- _ ] => invc $h; ff
-      end); ff u;
+      end); ff with u;
       repeat (rewrite length_app in *); ff;
       repeat (find_eapply_lem_hyp equiv_EvidenceT_impl_et_size_same); ff.
 Qed.
 
+Lemma wf_Evidence_proc_left : forall G e ep,
+  wf_Evidence G e ->
+  wf_Evidence G (proc_ev_path_left_ev ep e).
+Proof.
+  destruct ep; ff; eapply wf_Evidence_mt_evc.
+Qed.
+
+Lemma wf_Evidence_proc_right : forall G e ep,
+  wf_Evidence G e ->
+  wf_Evidence G (proc_ev_path_right_ev ep e).
+Proof.
+  destruct ep; ff; eapply wf_Evidence_mt_evc.
+Qed.
+
 (** * Theorem:  CVM execution preserves well-formedness of Evidence bundles 
       (EvidenceT Type of sufficient length for raw EvidenceT). *)
 Theorem cvm_preserves_wf_Evidence : forall t st st' e e' sc,
@@ -985,8 +971,7 @@ Theorem cvm_preserves_wf_Evidence : forall t st st' e e' sc,
   build_cvm e t sc st = (res e', st') ->
   wf_Evidence (session_context sc) e'.
 Proof.
-  induction t; simpl in *; intuition;
-  cvm_monad_unfold; try (ff a; fail).
+  induction t; simpl in *; intros; cvm_monad_unfold.
   - ff;
     try (match! goal with
     | [ |- wf_Evidence _ mt_evc ] => eapply wf_Evidence_mt_evc
@@ -998,28 +983,28 @@ Proof.
       econstructor; ff;
       repeat find_rewrite;
       repeat find_injection;
-      ff u;
+      ff with u;
       repeat (rewrite length_app in *);
       f_equal; lia).
     eapply wf_Evidence_invoke_APPR; eauto; destruct e; ff.
   - ff;
     find_eapply_lem_hyp do_remote_res_axiom; eauto; ff.
     Unshelve. 
-    ref (Build_Session_Config "" (Build_GlobalContext _ [] []) (fun _ _ => res []) [] [] []).
     eapply 0.
+  - ff.
   - ff; simpl in *.
-    eapply IHt1 in Heqp; ff; eauto with wf_Evidence.
+    eapply IHt1 in Heq > [ | eapply wf_Evidence_proc_left; ff ].
+    eapply IHt2 in Heq0 > [ | eapply wf_Evidence_proc_right; ff ].
+    ff; eauto with wf_Evidence.
   - ff; simpl in *.
     find_eapply_lem_hyp parallel_vm_thread_axiom; ff.
-    eapply IHt1 in Heqp; ff; eauto with wf_Evidence.
-    eapply IHt2 in H0; ff; eauto with wf_Evidence.
-    destruct s, s, s0; ff; 
-    unfold mt_evc in *; ff;
-    eauto with wf_Evidence;
-    econstructor; ff l.
-    Unshelve.
-    eapply 0.
-    eapply 0.
+    eapply IHt1 in Heq > [ | eapply wf_Evidence_proc_left; ff ].
+    destruct e;
+    ff; eauto with wf_Evidence.
+
+    eapply IHt2 in Hex;
+    ff; eauto with wf_Evidence.
+    eapply wf_Evidence_mt_evc.
 Qed.
 
 Theorem invoke_APPR_respects_events : forall G et r eo st sc st' e' i m evs,
@@ -1036,7 +1021,7 @@ Proof.
   simpl in *; intros; cvm_monad_unfold.
   - ff; rewrite app_nil_r; ff.
   - ff. 
-  - ff u;
+  - ff with u;
     repeat (find_eapply_lem_hyp peel_n_rawev_result_spec); ff;
     try (match! goal with
     | [ h : invoke_APPR' _ ?_e _ _ _ = _,
@@ -1051,7 +1036,7 @@ Proof.
     end;
     assert (st_evid st + 1 + 1 = st_evid st + 2) by lia; ff;
     repeat (rewrite <- app_assoc); ff).
-  - ff u;
+  - ff with u;
     repeat (find_eapply_lem_hyp peel_n_rawev_result_spec); ff;
     try (match! goal with
     | [ h : invoke_APPR' _ ?_e _ _ _ = _,
@@ -1066,8 +1051,8 @@ Proof.
     end;
     assert (st_evid st + 1 + 1 = st_evid st + 2) by lia; ff;
     repeat (rewrite <- app_assoc); ff);
-    ateb_same; ff a.
-  - ff u;
+    ateb_same; ff with a.
+  - ff with u;
     repeat (find_eapply_lem_hyp peel_n_rawev_result_spec); ff;
     try (match! goal with
     | [ h : invoke_APPR' _ ?_e _ _ _ = _,
@@ -1082,7 +1067,7 @@ Proof.
     end;
     assert (st_evid st + 1 + 1 = st_evid st + 2) by lia; ff;
     repeat (rewrite <- app_assoc); ff).
-  - ff u;
+  - ff with u;
     repeat (find_eapply_lem_hyp peel_n_rawev_result_spec); ff;
     try (match! goal with
     | [ h : invoke_APPR' _ ?_e _ _ _ = _,
@@ -1097,8 +1082,8 @@ Proof.
     end;
     assert (st_evid st + 1 + 1 = st_evid st + 2) by lia; ff;
     repeat (rewrite <- app_assoc); ff);
-    ateb_same; ff a.
-  - ff u;
+    ateb_same; ff with a.
+  - ff with u;
     repeat (find_eapply_lem_hyp peel_n_rawev_result_spec); ff;
     try (match! goal with
     | [ h : invoke_APPR' _ ?_e _ _ _ = _,
@@ -1113,8 +1098,8 @@ Proof.
     end;
     assert (st_evid st + 1 + 1 = st_evid st + 2) by lia; ff;
     repeat (rewrite <- app_assoc); ff);
-    ateb_same; ff a.
-  - ff u;
+    ateb_same; ff with a.
+  - ff with u;
     repeat (match! goal with
     | [ h : invoke_APPR' _ ?_e _ _ _ = _,
         h2 : appr_events' _ _ ?_e _ _ = _,
@@ -1124,9 +1109,9 @@ Proof.
       eapply invoke_APPR'_spans in $h as ?; try reflexivity; ff;
       try (eapply appr_events'_size_works; eauto; ff); ff;
       eapply $ih in $h > [ | | | | | eapply $h2 ]; 
-      simpl in *; try reflexivity; ff l
+      simpl in *; try reflexivity; ff with l
     end);
-    repeat (rewrite <- app_assoc); ff l.
+    repeat (rewrite <- app_assoc); ff with l.
 Qed.
 
 (** * Main Theorem: CVM traces are respected the reference "events"
@@ -1154,7 +1139,7 @@ Proof.
     try (match! goal with
     | [ e : EvidenceT |- _ ] => 
       let e := Control.hyp e in
-      induction $e; simpl in *; ff a; fail
+      induction $e; simpl in *; ff with a; fail
     end).
     eapply invoke_APPR_respects_events in H4; ff.
   - ff; invc H0; cvm_monad_unfold; ff;
@@ -1168,7 +1153,6 @@ Proof.
     repeat (rewrite <- app_assoc); eauto.
     find_eapply_lem_hyp do_remote_res_axiom; ff.
     find_eapply_lem_hyp cvm_evidence_type; ff.
-    repeat (find_higher_order_rewrite); ff.
     Unshelve. eapply 0.
 
   - ff; cvm_monad_unfold; ff.
@@ -1178,52 +1162,47 @@ Proof.
     end; cvm_monad_unfold; ff;
     simpl in *; repeat find_rewrite;
     repeat find_injection; ff.
-    eapply IHt1 in Heqp as ?; eauto;
-    eapply cvm_evidence_type in Heqp as ?; ff.
+    eapply IHt1 in Heq as ?; eauto;
+    eapply cvm_evidence_type in Heq as ?; ff.
     rewrite app_assoc. 
     rewrite <- H0.
     eapply IHt2 in H4; ff.
     eapply cvm_spans; ff;
     eapply events_range; eauto.
-  - ff a;
+  - destruct e; Control.enter (fun () => ff with a;
     match! goal with
     | [ h : events _ _ _ _ |- _ ] => 
       invc $h; ff
     end; cvm_monad_unfold; ff;
-    cvm_monad_unfold; ff a.
-    eapply IHt1 in Heqp as ?; eauto;
+    cvm_monad_unfold; ff with a;
+    eapply IHt1 in Heq as ?; eauto;
     try (destruct s, s, s0; ff; fail);
-    eapply cvm_spans in Heqp as ?; eauto; ff;
+    eapply cvm_spans in Heq as ?; eauto; ff;
     try (repeat find_rewrite; simpl in *;
-      destruct s, s, s0; simpl in *; 
       eapply events_range; eauto; ff; fail); 
-    ff.
-    eapply IHt2 in Heqp0 as ? > [ | | destruct s, s, s0; ff | | | ]; ff.
+    ff;
+    eapply IHt2 in Heq0 as ? > [ | | | | | ]; ff;
     repeat (erewrite <- app_assoc); ff;
     find_eapply_lem_hyp cvm_spans; ff;
-    destruct s, s, s0; ff;
-    eapply events_range; eauto; ff a.
-  - ff a; invc H0; ff a;
-    cvm_monad_unfold; ff a;
+    eapply events_range; eauto; ff with a).
+  - destruct e; Control.enter (fun () =>
+    ff with a; invc H0; ff with a;
+    cvm_monad_unfold; ff with a;
     simpl in *; repeat find_rewrite;
-    repeat find_injection; ff.
-    eapply IHt1 in Heqp as ?; try (destruct s, s, s0; ff; fail); eauto; ff; try lia.
-    eapply cvm_spans in Heqp as ?; eauto; ff;
+    repeat find_injection; ff;
+    eapply IHt1 in Heq as ?; eauto; ff; try lia;
+    eapply cvm_spans in Heq as ?; eauto; ff;
     try (repeat find_rewrite; simpl in *;
-      destruct s, s, s0; simpl in *; 
       eapply events_range; eauto; ff; fail);
-    repeat find_rewrite; try lia.
-    repeat (rewrite <- app_assoc); simpl in *; ff.
-    repeat find_rewrite; repeat find_injection; eauto.
-    assert (st_evid st + 2 + List.length evs1 = st_evid st + 1 + 1 + List.length evs1) by lia.
-    ff.
-    erewrite events_events_fix_eq in *; ff.
-    assert (n = List.length evs2). {
-      repeat (find_eapply_lem_hyp events_fix_range); eauto; ff;
-      destruct s, s, s0; ff; unfold mt_evc in *; simpl in *; ff.
-    }
-    ff.
-    destruct s, s, s0; ff; unfold mt_evc in *; simpl in *; ff.
+    repeat find_rewrite; try lia;
+    repeat (rewrite <- app_assoc); simpl in *; ff;
+    repeat find_rewrite; repeat find_injection; eauto;
+    assert (st_evid st + 2 + List.length evs1 = st_evid st + 1 + 1 + List.length evs1) by lia;
+    ff;
+    erewrite events_events_fix_eq in *; ff;
+    assert (n = List.length evs2) by (
+      repeat (find_eapply_lem_hyp events_fix_range); eauto; ff);
+    ff).
 Qed.
 
 Corollary cvm_trace_respects_events_default : forall G,