diff --git a/deps/cryptol b/deps/cryptol
index 34404d7930..08cd609c4c 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit 34404d7930d82b8b96c5ccc32d8ae5a7ba033e5e
+Subproject commit 08cd609c4c58ebb5a4cd22ad053d8255ce8d1fc5
diff --git a/heapster-saw/examples/_CoqProject b/heapster-saw/examples/_CoqProject
index ecaa39363a..116ab8ed3c 100644
--- a/heapster-saw/examples/_CoqProject
+++ b/heapster-saw/examples/_CoqProject
@@ -32,5 +32,7 @@ exp_explosion_gen.v
 exp_explosion_proofs.v
 mbox_gen.v
 mbox_proofs.v
+global_var_gen.v
+global_var_proofs.v
 sha512_gen.v
 #sha512_proofs.v
diff --git a/heapster-saw/examples/global_var.bc b/heapster-saw/examples/global_var.bc
new file mode 100644
index 0000000000..0cb09c9699
Binary files /dev/null and b/heapster-saw/examples/global_var.bc differ
diff --git a/heapster-saw/examples/global_var.c b/heapster-saw/examples/global_var.c
new file mode 100644
index 0000000000..6975003bce
--- /dev/null
+++ b/heapster-saw/examples/global_var.c
@@ -0,0 +1,56 @@
+#include <stdlib.h>
+#include <stdint.h>
+
+/* A very simple acquire/release lock for some shared data */
+
+int64_t shared_data = 0;
+int64_t lock = 0;
+
+/* A spin lock; returns 1 after acquireing lock, otherwise runs forever.
+   (Not robust to concurrent semantics) */
+int64_t acquire_lock(int64_t** data) {
+  while (lock != 0) {
+    continue;
+ }
+  lock = 1;
+  *data = &shared_data;
+  return 1;
+}
+
+/* To be called after a thread is done accessing the shared data. */ 
+void release_lock(void) {
+  lock = 0;
+  return;
+}
+
+
+int64_t acquire_release_acquire_release(void) {
+
+  int64_t* data;
+  acquire_lock(&data);
+  *data = 42;
+  release_lock();
+  
+  acquire_lock(&data);
+  if (data == NULL) {
+    return -1;
+  }
+  int64_t val = *data;
+  release_lock();
+  return val;
+}
+
+int64_t acquire_release_fail(void) {
+  int64_t* data;
+  acquire_lock(&data);
+  *data = 42;
+  release_lock();
+
+  *data = 84;
+
+  // shared data should still be 42
+  acquire_lock(&data);
+  int64_t val = *data;
+  release_lock();
+  return val;
+}
diff --git a/heapster-saw/examples/global_var.saw b/heapster-saw/examples/global_var.saw
new file mode 100644
index 0000000000..597f7c5f6d
--- /dev/null
+++ b/heapster-saw/examples/global_var.saw
@@ -0,0 +1,73 @@
+enable_experimental;
+env <- heapster_init_env_from_file "global_var.sawcore" "global_var.bc";
+
+// Integer types
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+
+
+// Demonstrates one technique for dealing with global variables and environment
+// permissions like locks
+
+
+
+// A heapster type for the lock global variable"
+//
+// The rwmodality makes the permission not copyable when provided the write
+// modality.
+//
+// When extracted to Coq, u:has_lock_perm<W> and u:can_lock_perm<W> are
+// bitvectors representing the value stored in the shared_data variable
+heapster_define_opaque_perm env "has_lock_perm"
+    "rw:rwmodality, dat:llvmptr 64"
+    "unit"
+    "Vec 64 Bool";
+
+heapster_define_opaque_perm env "can_lock_perm"
+    "rw:rwmodality"
+    "unit"
+    "Vec 64 Bool";
+
+// Need to axiomatize acquire_lock because it touches the global variables
+heapster_assume_fun env
+    "acquire_lock"
+
+    "(u:unit). \
+    \ arg0:ptr((W,0) |-> true), \
+    \ u:can_lock_perm<W> \
+    \ -o \
+    \ (dat:llvmptr 64). \
+    \ ret:eq(llvmword(1)), \
+    \ arg0:ptr((W,0) |-> eq(dat)), \
+    \ dat:ptr((W,0) |-> int64<>), \
+    \ u:has_lock_perm<W,dat>"
+
+    "acquireLockM";
+
+heapster_assume_fun env
+    "release_lock"
+
+    "(u:unit, dat:llvmptr 64). \
+    \ u:has_lock_perm<W,dat>, \
+    \ dat:ptr((W,0) |-> int64<>) \
+    \ -o \
+    \ ret:true, \
+    \ u:can_lock_perm<W>"
+
+    "releaseLockM";
+
+
+
+heapster_typecheck_fun env
+    "acquire_release_acquire_release"
+    "(u:unit). u:can_lock_perm<W> \
+    \ -o \
+    \ ret:int64<>, u:can_lock_perm<W>";
+
+heapster_typecheck_fun env
+    "acquire_release_fail"
+    "(u:unit). u:can_lock_perm<W> \
+    \ -o \
+    \ ret:int64<>, u:can_lock_perm<W>";
+    
+
+heapster_export_coq env "global_var_gen.v";
diff --git a/heapster-saw/examples/global_var.sawcore b/heapster-saw/examples/global_var.sawcore
new file mode 100644
index 0000000000..a1f63d7f19
--- /dev/null
+++ b/heapster-saw/examples/global_var.sawcore
@@ -0,0 +1,10 @@
+module GlobalVar where
+
+import Prelude;
+
+acquireLockM : Vec 64 Bool -> CompM (Vec 64 Bool * Vec 64 Bool);
+acquireLockM u = returnM (Vec 64 Bool * Vec 64 Bool)
+			 (u,u);
+
+releaseLockM : Vec 64 Bool -> Vec 64 Bool -> CompM (Vec 64 Bool);
+releaseLockM u new_u = returnM (Vec 64 Bool) new_u;
diff --git a/heapster-saw/examples/global_var_proofs.v b/heapster-saw/examples/global_var_proofs.v
new file mode 100644
index 0000000000..7011518cf0
--- /dev/null
+++ b/heapster-saw/examples/global_var_proofs.v
@@ -0,0 +1,56 @@
+From Coq          Require Import Lists.List.
+From Coq          Require Import String.
+From Coq          Require Import Vectors.Vector.
+From CryptolToCoq Require Import SAWCoreScaffolding.
+From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
+From CryptolToCoq Require Import SAWCoreBitvectors.
+From CryptolToCoq Require Import SAWCorePrelude.
+From CryptolToCoq Require Import CompMExtra.
+
+
+
+Require Import Examples.global_var_gen.
+Import GlobalVar.
+
+Import SAWCorePrelude.
+
+Lemma no_errors_acquire_release_acquire_release :
+    refinesFun acquire_release_acquire_release (fun _ => noErrorsSpec).
+Proof.
+    unfold acquire_release_acquire_release,
+           acquire_release_acquire_release__tuple_fun,
+           noErrorsSpec,
+           acquireLockM, releaseLockM.
+    prove_refinement.
+Qed.
+    
+
+Definition acquire_release_acquire_release_spec (x : bitvector 64)
+    : CompM (can_lock_perm * bitvector 64) :=
+    returnM (intToBv 64 42, intToBv 64 42).
+
+Lemma spec_acquire_release_acquire_release :
+        refinesFun acquire_release_acquire_release
+                   acquire_release_acquire_release_spec.
+Proof.
+    unfold acquire_release_acquire_release,
+           acquire_release_acquire_release__tuple_fun,
+           acquire_release_acquire_release_spec,
+           acquireLockM, releaseLockM,
+           projT2.
+    prove_refinement.
+Qed.
+
+
+Definition errorSpec {A} : CompM A := existsM (fun (s : string) => errorM s).
+
+Lemma errors_acquire_release_fail : refinesFun acquire_release_fail
+                                               (fun _ => errorSpec).
+Proof.
+    unfold acquire_release_fail, acquire_release_fail__tuple_fun,
+           errorSpec,
+           acquireLockM, releaseLockM,
+           projT2.
+    prove_refinement.
+Qed.
+    
diff --git a/heapster-saw/examples/mbox_proofs.v b/heapster-saw/examples/mbox_proofs.v
index def38151e9..21adb254ed 100644
--- a/heapster-saw/examples/mbox_proofs.v
+++ b/heapster-saw/examples/mbox_proofs.v
@@ -382,8 +382,8 @@ Proof.
   (* Most of the remaining cases are taken care of with just bvAdd_id_l and bvAdd_id_r *)
   all: try rewrite bvAdd_id_r; try rewrite bvAdd_id_l; try reflexivity.
   (* The remaining case just needs a few more rewrites *)
-  - rewrite bvAdd_assoc, bvAdd_comm, bvAdd_assoc; reflexivity.
-  - cbn; rewrite transMbox_Mbox_nil_r; reflexivity.
+  - simpl. f_equal. rewrite bvAdd_assoc. f_equal. rewrite bvAdd_comm. f_equal.
+    simpl. rewrite transMbox_Mbox_nil_r. reflexivity.
 Time Qed.
 
 
@@ -467,6 +467,7 @@ Proof.
   - rewrite e_forall0 in e_maybe0.
     discriminate e_maybe0.
   (* TODO Add the sort of reasoning in the next two cases back into the automation? *)
+
   - rewrite a in e_maybe1.
     discriminate e_maybe1.
   - rewrite a1 in e_maybe2.
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 594b91f78d..a50a3b9d21 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -31,7 +31,6 @@ module Verifier.SAW.Heapster.Implication where
 
 import Data.Maybe
 import Data.List
-import Data.Functor.Product
 import Data.Functor.Compose
 import Data.Reflection
 import qualified Data.BitVector.Sized as BV
@@ -65,6 +64,7 @@ import Verifier.SAW.Heapster.Permissions
 import Verifier.SAW.Heapster.GenMonad
 
 import GHC.Stack
+import Unsafe.Coerce
 
 
 -- * Helper functions (should be moved to Hobbits)
@@ -170,6 +170,12 @@ eqProofStepLiftA2 f (EqProofStep eq_perms1 g1) (EqProofStep eq_perms2 g2) =
   let (es1, es2) = RL.split eq_perms1 eq_perms2 es in
   f (g1 es1) (g2 es2)
 
+-- | Build an 'EqProofStep' for @(e1,...,en)=(x1,...,xn)@ from permissions
+-- @x1:eq(e1),...,xn:eq(en)@
+eqProofStepFromPermsRev :: RAssign ExprVar as -> PermExprs as ->
+                           EqProofStep as (PermExprs as)
+eqProofStepFromPermsRev xs es =
+  EqProofStep (RL.map2 (\x e -> EqPerm x e False) xs es) id
 
 -- | A proof that two objects are equal, using 0 or more 'EqProofStep' steps
 data EqProof ps a where
@@ -208,6 +214,18 @@ eqProofPerms (EqProofRefl _) = DistPermsNil
 eqProofPerms (EqProofCons eqp eq_step) =
   appendDistPerms (eqProofPerms eqp) (eqProofStepPerms eq_step)
 
+-- | Build an 'EqProof' from a single 'EqProofStep'
+eqProofFromStep :: EqProofStep ps a -> EqProof ps a
+eqProofFromStep eq_step
+  | Refl <- RL.prependRNilEq (eqProofStepPerms eq_step)
+  = EqProofCons (EqProofRefl $ eqProofStepLHS eq_step) eq_step
+
+-- | Build an 'EqProof' that @(e1,...,en)=(x1,...,xn)@ from permissions
+-- @x1:eq(e1),...,xn:eq(en)@
+eqProofFromPermsRev :: RAssign ExprVar as -> PermExprs as ->
+                       EqProof as (PermExprs as)
+eqProofFromPermsRev xs es = eqProofFromStep $ eqProofStepFromPermsRev xs es
+
 instance Functor (EqProof ps) where
   fmap f (EqProofRefl a) = EqProofRefl $ f a
   fmap f (EqProofCons eqp eq_step) =
@@ -235,6 +253,15 @@ someEqProofPerms (SomeEqProofCons some_eqp eq_step)
   | Some ps <- someEqProofPerms some_eqp =
     Some (RL.append ps $ eqProofStepPerms eq_step)
 
+someEqProofPP :: PermPretty a => PPInfo -> SomeEqProof a -> Doc ann
+someEqProofPP i pf =
+                pretty "SomeEqProof:"
+                <+> permPretty i (someEqProofLHS pf)
+                <+> pretty "="
+                <+> permPretty i (someEqProofRHS pf)
+                <+> line
+                <+> permPretty i (someEqProofPerms pf)
+
 -- | Construct a 'SomeEqProof' for @x=e@ or @e=x@ using an @x:eq(e)@ permission,
 -- where the 'Bool' flag is 'True' for @x=e@ and 'False' for @e=x@ like 'EqPerm'
 someEqProof1 :: ExprVar a -> PermExpr a -> Bool -> SomeEqProof (PermExpr a)
@@ -347,6 +374,16 @@ unSomeEqProof (SomeEqProofCons some_eqp eq_step)
 --
 -- where the types of @P1@ through @Pn@ are given by the first type argument
 -- @ps_in@ and those of @P1'@ through @Pm'@ are given by the second, @ps_out@.
+--
+-- To add a new @SimplImpl@ proof rule:
+-- 1. Add a constructor @SImpl_NewConstructor@ and documentation to this
+--    data structure
+-- 2. Implement cases for the helper functions @simplImplIn@,
+--    @simplImplOut@, and @genSubst@ for @SImpl_NewConstructor@
+-- 3. Implement a wrapper @newConstructorM@ using @implSimplM@ to build up a
+--    proof using that constructor in the @ImplM@ monad
+-- 4. Implement the translation of the constructor by adding a case to
+--    `translateSimplImpl` in `SAWTranslation.hs`.
 data SimplImpl ps_in ps_out where
   -- | Drop a permission, i.e., forget about it:
   --
@@ -409,9 +446,9 @@ data SimplImpl ps_in ps_out where
   -- | Cast a proof of @x:p@ to one of @x:p'@ using a proof that @p=p'@ along
   -- with the equality permissions needed by that proof:
   --
-  -- > x1:eq(e1), ..., xn:eq(en), x:p -o x:p'
+  -- > x:p, x1:eq(e1), ..., xn:eq(en) -o x:p', x1:eq(e1), ..., xn:eq(en)
   SImpl_CastPerm :: ExprVar a -> EqProof ps (ValuePerm a) ->
-                    SimplImpl (RNil :> a :++: ps) (RNil :> a)
+                    SimplImpl (RNil :> a :++: ps) (RNil :> a :++: ps)
 
   -- | Introduce a proof that @x:eq(x)@:
   --
@@ -431,6 +468,13 @@ data SimplImpl ps_in ps_out where
   SImpl_InvTransEq :: ExprVar a -> ExprVar a -> PermExpr a ->
                       SimplImpl (RNil :> a :> a) (RNil :> a)
 
+  -- | For any unit-typed variable @x@ and unit-type expression @e@, prove
+  -- @x:eq(e)@
+  -- 
+  -- > (x:unit,e:unit) . -o x:eq(e)
+  SImpl_UnitEq :: ExprVar UnitType -> PermExpr UnitType ->
+                  SimplImpl RNil (RNil :> UnitType)
+
   -- FIXME HERE: remove this in favor of SImpl_Copy
 
   -- | Copy an equality proof on the top of the stack:
@@ -1245,6 +1289,17 @@ data SimplImpl ps_in ps_out where
 --
 -- where each @bsi@ is itself an 'RList' of the types of the bound variables in
 -- @zsi@ and @psi@ is an 'RList' of the types of @Pi_1@ through @Pi_km@.
+--
+-- To add a new @PermImpl1@ proof rule:
+-- 1. Add a constructor @Impl1_NewConstructor@ and documentation to this
+--    data structure
+-- 2. Implement cases for the helper functions @permImplStep@,
+--   @permImplSucceeds@, @applyImpl1@, and @genSubst@ for
+--   @Impl1_NewConstructor@
+-- 3. Implement a wrapper @newConstructorM@ using @implApplyImpl1@ to build
+--    up a proof using that constructor in the @ImplM@ monad
+-- 4. Implement the translation of the constructor by adding a case to
+--    `translatePermImpl1` in `SAWTranslation.hs`.
 data PermImpl1 ps_in ps_outs where
   -- | Failure of a permission implication, along with a string explanation of
   -- the failure, which is a proof of 0 disjuncts:
@@ -1717,6 +1772,7 @@ simplImplIn (SImpl_IntroEqRefl _) = DistPermsNil
 simplImplIn (SImpl_InvertEq x y) = distPerms1 x (ValPerm_Eq $ PExpr_Var y)
 simplImplIn (SImpl_InvTransEq x y e) =
   distPerms2 x (ValPerm_Eq e) y (ValPerm_Eq e)
+simplImplIn (SImpl_UnitEq _ _) = DistPermsNil
 simplImplIn (SImpl_CopyEq x e) = distPerms1 x (ValPerm_Eq e)
 simplImplIn (SImpl_LLVMWordEq x y e) =
   distPerms2 x (ValPerm_Eq (PExpr_LLVMWord (PExpr_Var y))) y (ValPerm_Eq e)
@@ -2011,10 +2067,12 @@ simplImplOut (SImpl_IntroOrL x p1 p2) = distPerms1 x (ValPerm_Or p1 p2)
 simplImplOut (SImpl_IntroOrR x p1 p2) = distPerms1 x (ValPerm_Or p1 p2)
 simplImplOut (SImpl_IntroExists x _ p) = distPerms1 x (ValPerm_Exists p)
 simplImplOut (SImpl_Cast x _ p) = distPerms1 x p
-simplImplOut (SImpl_CastPerm x eqp) = distPerms1 x (eqProofRHS eqp)
+simplImplOut (SImpl_CastPerm x eqp) =
+  appendDistPerms (distPerms1 x (eqProofRHS eqp)) (eqProofPerms eqp)
 simplImplOut (SImpl_IntroEqRefl x) = distPerms1 x (ValPerm_Eq $ PExpr_Var x)
 simplImplOut (SImpl_InvertEq x y) = distPerms1 y (ValPerm_Eq $ PExpr_Var x)
 simplImplOut (SImpl_InvTransEq x y _) = distPerms1 x (ValPerm_Eq $ PExpr_Var y)
+simplImplOut (SImpl_UnitEq x e) = distPerms1 x (ValPerm_Eq e)
 simplImplOut (SImpl_CopyEq x e) = distPerms2 x (ValPerm_Eq e) x (ValPerm_Eq e)
 simplImplOut (SImpl_LLVMWordEq x _ e) =
   distPerms1 x (ValPerm_Eq (PExpr_LLVMWord e))
@@ -2619,6 +2677,8 @@ instance SubstVar PermVarSubst m =>
       SImpl_InvertEq <$> genSubst s x <*> genSubst s y
     [nuMP| SImpl_InvTransEq x y e |] ->
       SImpl_InvTransEq <$> genSubst s x <*> genSubst s y <*> genSubst s e
+    [nuMP| SImpl_UnitEq x e |] ->
+      SImpl_UnitEq <$> genSubst s x <*> genSubst s e
     [nuMP| SImpl_CopyEq x e |] ->
       SImpl_CopyEq <$> genSubst s x <*> genSubst s e
     [nuMP| SImpl_LLVMWordEq x y e |] ->
@@ -2918,9 +2978,15 @@ instance SubstVar s m => Substable1 s (LocalImplRet ps) m where
 
 data ImplState vars ps =
   ImplState { _implStatePerms :: PermSet ps,
+              -- ^ The current primary permissions and permissions stack
               _implStateVars :: CruCtx vars,
+              -- ^ The types of all evars in scope
               _implStatePSubst :: PartialSubst vars,
+              -- ^ The partial instantiation of evars in scope
               _implStatePVarSubst :: RAssign (Compose Maybe ExprVar) vars,
+              -- ^ The partial instantiation of evars to fresh variables; used
+              -- by 'proveVarsImplVarEVars' and when evars need have permissions
+              -- proved on them
               _implStateRecRecurseFlag :: RecurseFlag,
               -- ^ Whether we are recursing under a recursive permission, either
               -- on the left hand or the right hand side
@@ -2930,6 +2996,9 @@ data ImplState vars ps =
               -- ^ Pretty-printing for all variables in scope
               _implStateNameTypes :: NameMap TypeRepr,
               -- ^ Types of all the variables in scope
+              _implStateUnitVar :: Maybe (ExprVar UnitType),
+              -- ^ A global unit variable that all other unit variables will be
+              -- equal to
               _implStateEndianness :: EndianForm,
               -- ^ The endianness of the current architecture
               _implStateFailPrefix :: String,
@@ -2940,9 +3009,10 @@ data ImplState vars ps =
 makeLenses ''ImplState
 
 mkImplState :: CruCtx vars -> PermSet ps -> PermEnv ->
-               PPInfo -> String -> DebugLevel -> NameMap TypeRepr ->
+               PPInfo -> String -> DebugLevel ->
+               NameMap TypeRepr -> Maybe (ExprVar UnitType) ->
                EndianForm -> ImplState vars ps
-mkImplState vars perms env info fail_prefix dlevel nameTypes endianness =
+mkImplState vars perms env info fail_prefix dlevel nameTypes u endianness =
   ImplState {
   _implStateVars = vars,
   _implStatePerms = perms,
@@ -2952,6 +3022,7 @@ mkImplState vars perms env info fail_prefix dlevel nameTypes endianness =
   _implStatePermEnv = env,
   _implStatePPInfo = info,
   _implStateNameTypes = nameTypes,
+  _implStateUnitVar = u,
   _implStateEndianness = endianness,
   _implStateFailPrefix = fail_prefix,
   _implStateDebugLevel = dlevel
@@ -2970,6 +3041,7 @@ unextImplState s =
       _implStatePSubst = unextPSubst (_implStatePSubst s),
       _implStatePVarSubst = RL.tail (_implStatePVarSubst s) }
 
+
 -- | The implication monad is a state-continuation monad that uses 'ImplState'
 type ImplM vars s r ps_out ps_in =
   GenStateContT
@@ -2980,54 +3052,67 @@ type ImplM vars s r ps_out ps_in =
 -- | Run an 'ImplM' computation by passing it a @vars@ context, a starting
 -- permission set, top-level state, and a continuation to consume the output
 runImplM ::
-  CruCtx vars ->
+  NuMatchingAny1 r =>
+  CruCtx vars               {- ^ existential variables and their types -} ->
   PermSet ps_in ->
   PermEnv                   {- ^ permission environment   -} ->
   PPInfo                    {- ^ pretty-printer settings  -} ->
   String                    {- ^ fail prefix              -} ->
   DebugLevel                {- ^ debug level              -} ->
   NameMap TypeRepr          {- ^ name types               -} ->
+  Maybe (ExprVar UnitType)  {- ^ optional global unit var -} ->
   EndianForm                {- ^ endianness               -} ->
   ImplM vars s r ps_out ps_in a ->
   ((a, ImplState vars ps_out) -> State (Closed s) (r ps_out)) ->
   State (Closed s) (PermImpl r ps_in)
-runImplM vars perms env ppInfo fail_prefix dlevel nameTypes endianness m k =
+runImplM vars perms env ppInfo fail_prefix dlevel nameTypes unitVar endianness m k =
   runGenStateContT
-    m
-    (mkImplState vars perms env ppInfo fail_prefix dlevel nameTypes endianness)
+    -- instantiate all unit evars to the global unit variable (with
+    -- 'handleUnitEVars') before running m
+    (handleUnitEVars >>> m)
+    (mkImplState vars perms env ppInfo fail_prefix dlevel nameTypes unitVar endianness)
     (\s a -> PermImpl_Done <$> k (a, s))
 
+
+
 -- | Run an 'ImplM' computation that returns a 'PermImpl', by inserting that
 -- 'PermImpl' inside of the larger 'PermImpl' that is built up by the 'ImplM'
 -- computation.
-runImplImplM :: CruCtx vars -> PermSet ps_in -> PermEnv -> PPInfo ->
-                String -> DebugLevel -> NameMap TypeRepr -> EndianForm ->
+runImplImplM :: NuMatchingAny1 r =>
+                CruCtx vars -> PermSet ps_in -> PermEnv -> PPInfo ->
+                String -> DebugLevel -> NameMap TypeRepr ->
+                Maybe (ExprVar UnitType) -> EndianForm ->
                 ImplM vars s r ps_out ps_in (PermImpl r ps_out) ->
                 State (Closed s) (PermImpl r ps_in)
-runImplImplM vars perms env ppInfo fail_prefix dlevel nameTypes endianness m =
+runImplImplM vars perms env ppInfo fail_prefix dlevel nameTypes u endianness m =
   runGenStateContT
-    m
-    (mkImplState vars perms env ppInfo fail_prefix dlevel nameTypes endianness)
+    -- instantiate all unit evars to the global unit variable (with
+    -- 'handleUnitEVars') before running m
+    (handleUnitEVars >>> m)
+    (mkImplState vars perms env ppInfo fail_prefix dlevel nameTypes u endianness)
     (\_ -> pure)
 
 -- | Embed a sub-computation in a name-binding inside another 'ImplM'
 -- computation, throwing away any state from that sub-computation and returning
 -- a 'PermImpl' inside a name-binding
-embedImplM :: DistPerms ps_in ->
+embedImplM :: NuMatchingAny1 r' =>
+              DistPerms ps_in ->
               ImplM RNil s r' ps_out ps_in (r' ps_out) ->
               ImplM vars s r ps ps (PermImpl r' ps_in)
 embedImplM ps_in m =
   get >>= \s ->
   lift $
   runImplM CruCtxNil (distPermSet ps_in)
-  (view implStatePermEnv s) (view implStatePPInfo s)
+  (view implStatePermEnv    s) (view implStatePPInfo     s)
   (view implStateFailPrefix s) (view implStateDebugLevel s)
-  (view implStateNameTypes s) (view implStateEndianness s) m (pure . fst)
+  (view implStateNameTypes  s) (view implStateUnitVar    s)
+  (view implStateEndianness s) m (pure . fst)
 
 -- | Embed a sub-computation in a name-binding inside another 'ImplM'
 -- computation, throwing away any state from that sub-computation and returning
 -- a 'PermImpl' inside a name-binding
-embedMbImplM :: KnownRepr CruCtx ctx => Mb ctx (DistPerms ps_in) ->
+embedMbImplM :: KnownRepr CruCtx ctx => NuMatchingAny1 r' =>
+                Mb ctx (DistPerms ps_in) ->
                 Mb ctx (ImplM RNil s r' ps_out ps_in (r' ps_out)) ->
                 ImplM vars s r ps ps (Mb ctx (PermImpl r' ps_in))
 embedMbImplM mb_ps_in mb_m =
@@ -3038,7 +3123,8 @@ embedMbImplM mb_ps_in mb_m =
          CruCtxNil (distPermSet ps_in)
          (view implStatePermEnv    s) (view implStatePPInfo  s)
          (view implStateFailPrefix s) (view implStateDebugLevel s)
-         (view implStateNameTypes  s) (view implStateEndianness s)
+         (view implStateNameTypes  s) (view implStateUnitVar s)
+         (view implStateEndianness s)
          (gmodify (over implStatePPInfo
                    (ppInfoAddTypedExprNames knownRepr ns)) >>>
           implSetNameTypes ns knownRepr >>>
@@ -3126,7 +3212,9 @@ getVarVarM memb =
   getPSubst >>>= \psubst ->
   use implStatePVarSubst >>>= \pvsubst ->
   case (RL.get memb pvsubst, psubstLookup psubst memb) of
-    (Compose (Just n), _) -> pure n
+    (Compose (Just n), Just _) -> pure n
+    (Compose (Just n), Nothing) ->
+      setVarM memb (PExpr_Var n) >>> pure n
     (_, Just e) ->
       getExVarType memb >>>= \tp ->
       implLetBindVar tp e >>>= \n ->
@@ -3138,20 +3226,27 @@ getVarVarM memb =
 -- returning the optional expression it was bound to in the current partial
 -- substitution when it is done
 withExtVarsM :: KnownRepr TypeRepr tp =>
+                NuMatchingAny1 r =>
                 ImplM (vars :> tp) s r ps1 ps2 a ->
                 ImplM vars s r ps1 ps2 (a, PermExpr tp)
 withExtVarsM m =
-  gmodify extImplState   >>>
-  m                      >>>= \a ->
-  getPSubst              >>>= \psubst ->
-  gmodify unextImplState >>>
+  -- Add a new existential to the 'ImplState'
+  gmodify extImplState       >>>
+  -- If the new existential has type unit, instantiate it to the global unit
+  handleUnitEVar Member_Base >>>
+  -- Run the computation
+  m                          >>>= \a ->
+  getPSubst                  >>>= \psubst ->
+  -- Remove the existential after it has been instantiated
+  gmodify unextImplState     >>>
   pure (a, case psubstLookup psubst Member_Base of
              Just e -> e
              Nothing -> zeroOfType knownRepr)
 
 -- | Run an implication computation with an additional context of existential
 -- variables
-withExtVarsMultiM :: KnownCruCtx vars' ->
+withExtVarsMultiM :: NuMatchingAny1 r =>
+                     KnownCruCtx vars' ->
                      ImplM (vars :++: vars') s r ps1 ps2 a ->
                      ImplM vars s r ps1 ps2 a
 withExtVarsMultiM MNil m = m
@@ -3235,6 +3330,28 @@ implFindLOwnedPerms =
                   _ -> Nothing) <$>
   NameMap.assocs <$> view varPermMap <$> getPerms
 
+-- | Instantiate the current @implStateUnitVar@ with the given @ExprVar@ of type
+-- @UnitType@
+setUnitImplM :: Maybe (ExprVar UnitType) -> ImplM vars s r ps ps ()
+setUnitImplM e = do st <- get
+                    put st{ _implStateUnitVar = e }
+
+getUnitImplM :: ImplM vars s r ps ps (Maybe (ExprVar UnitType))
+getUnitImplM = do st <- get
+                  return $ _implStateUnitVar st
+
+-- | If the global unit varaible is not yet set, generate a fresh name and set
+-- it
+ensureUnitImplM :: NuMatchingAny1 r =>
+                   ImplM vars s r ps ps (ExprVar UnitType)
+ensureUnitImplM =
+  getUnitImplM >>>= \maybe_u ->
+  case maybe_u of
+    Nothing -> implIntroUnitVar >>>= \n ->
+               setUnitImplM (Just n) >>>
+               pure n
+    Just u  -> pure u
+
 -- | Look up the type of a free variable
 implGetVarType :: Name a -> ImplM vars s r ps ps (TypeRepr a)
 implGetVarType n =
@@ -3264,13 +3381,99 @@ implFindVarOfType tp =
 
 -- | Remember the types associated with a list of 'Name's, and also ensure those
 -- names have permissions
-implSetNameTypes :: RAssign Name ctx -> CruCtx ctx -> ImplM vars s r ps ps ()
+implSetNameTypes :: NuMatchingAny1 r =>
+                    RAssign Name ctx -> CruCtx ctx -> ImplM vars s r ps ps ()
 implSetNameTypes MNil _ = pure ()
 implSetNameTypes (ns :>: n) (CruCtxCons tps tp) =
   do implStateNameTypes %= NameMap.insert n tp
      implStatePerms     %= initVarPerm n
+     handleUnitVar tp n
      implSetNameTypes ns tps
 
+-- | When adding a new existential unit-typed variable, instantiate it with the
+-- underlying global unit if available; if not, update the global unit variable
+-- with a fresh variable
+handleUnitEVar :: forall (a :: CrucibleType) vars s r ps.
+                  NuMatchingAny1 r =>
+                  Member vars a -> ImplM vars s r ps ps ()
+-- Note: this only works in ImplM monad, not necessarily in TypedCrucible
+handleUnitEVar mem =
+  use implStateVars >>>= \vars ->
+  case cruCtxLookup vars mem of
+    UnitRepr -> -- get the global unit variable
+                ensureUnitImplM >>>= \u ->
+                -- add the binding mem |-> u to implStatePSubst
+                -- will fail if mem already is instantiated in implStatePSubst
+                modifyPSubst (psubstSet mem (PExpr_Var u))
+    _        -> -- non-unit variables
+                pure ()
+
+-- | Call handleUnitEVar on every existential variable in @vars@. Note that this
+-- will fail if called more than once on overlapping sets of @vars@.
+handleUnitEVars :: forall vars s r ps.
+                   NuMatchingAny1 r =>
+                   ImplM vars s r ps ps ()
+-- look up current cructx, then call handleUnitEVar for each member proof
+-- RL.members (CruCtxProxies vars)
+handleUnitEVars =
+    use implStateVars >>>= \vars ->
+    let mems :: RAssign (Member vars) vars
+        -- get the memberships of all variables
+        mems = RL.members (cruCtxProxies vars)
+    -- call handleUnitEVar on each variable
+    in RL.foldr handleUnitEVarM (pure ()) mems
+  where
+    handleUnitEVarM :: forall (a :: CrucibleType).
+                       Member vars a ->
+                       ImplM vars s r ps ps () ->
+                       ImplM vars s r ps ps ()
+    handleUnitEVarM mem m = handleUnitEVar mem >>> m
+
+
+-- | When adding a new universal unit-typed variable, unify with the underlying
+-- global unit if available, and if not, update the global unit variable with
+-- the variable provided
+handleUnitVar :: NuMatchingAny1 r =>
+                 TypeRepr a -> ExprVar a -> ImplM vars s r ps ps ()
+handleUnitVar UnitRepr n =
+  -- When introducing a new unit-typed variable, check whether we have a global
+  -- unit variable in the current @ImplState@
+  getUnitImplM >>= \u -> case u of
+    Nothing ->
+      -- If not, initialize the state with the current variable
+      setUnitImplM (Just n)
+    Just x | x == n ->
+      -- If n is equal to the global unit, do nothing
+      pure ()
+    Just x  ->
+      -- Otherwise, add a permission @n:eq(x)@, and then pop it off the stack
+        unitEqM n (PExpr_Var x) >>>
+        implPopM n (ValPerm_Eq (PExpr_Var x)) >>>
+        pure ()
+handleUnitVar _ _ = pure ()
+
+-- | Unify the unit variables already added to the state NameMap
+handleUnitVars :: forall (tps :: RList CrucibleType)
+                          vars r s ps.
+                  NuMatchingAny1 r =>
+                  RAssign Name tps ->
+                  ImplM vars s r ps ps ()
+handleUnitVars ns = use implStateNameTypes >>>= \nameMap ->
+                    handleUnitVars' nameMap ns
+
+handleUnitVars' :: forall (tps :: RList CrucibleType)
+                          vars r s ps.
+                   NuMatchingAny1 r =>
+                   NameMap TypeRepr ->
+                   RAssign Name tps ->
+                   ImplM vars s r ps ps ()
+handleUnitVars' _       MNil       = pure ()
+handleUnitVars' nameMap (ns :>: n) =
+  case NameMap.lookup n nameMap of
+    Nothing -> error "handleUnitVars: variable not added to nameMap"
+    Just tp -> handleUnitVar tp n >>>
+               handleUnitVars' nameMap ns
+
 
 ----------------------------------------------------------------------
 -- * The Permission Implication Rules as Monadic Operations
@@ -3294,7 +3497,8 @@ implApplyImpl1 impl1 mb_ms =
   gmapRet (PermImpl_Step impl1 <$>) >>>
   helper (applyImpl1 pp_info impl1 perms) mb_ms
   where
-    helper :: MbPermSets ps_outs ->
+    helper :: NuMatchingAny1 r =>
+              MbPermSets ps_outs ->
               RAssign (Impl1Cont vars s r ps_r a) ps_outs ->
               GenStateContT
                 (ImplState vars ps_r)  (PermImpl r ps_r)
@@ -3460,7 +3664,7 @@ implLetBindVar :: NuMatchingAny1 r => TypeRepr tp -> PermExpr tp ->
 implLetBindVar tp e =
   implApplyImpl1 (Impl1_LetBind tp e)
   (MNil :>: Impl1Cont (\(_ :>: n) -> pure n)) >>>= \n ->
-  implPopM n (ValPerm_Eq e) >>>
+  recombinePerm n (ValPerm_Eq e) >>>
   pure n
 
 -- | Bind a sequence of variables with 'implLetBindVar'
@@ -3470,6 +3674,24 @@ implLetBindVars CruCtxNil MNil = pure MNil
 implLetBindVars (CruCtxCons tps tp) (es :>: e) =
   (:>:) <$> implLetBindVars tps es <*> implLetBindVar tp e
 
+-- | Introduce a new univerally-quantified variable @x@ of unit type.
+--
+-- ps -o x. ps
+implIntroUnitVar :: NuMatchingAny1 r =>
+                    ImplM vars s r ps ps (Name UnitType)
+implIntroUnitVar =
+  -- Note that unlike @implLetbindVar@, this function does *not* bind @x@ to a
+  -- value @e@. Instead, we have almost the same operations as 'implLetBindVar'
+  -- but instead of calling 'recombinePerm', we instead call
+  -- 'implLetBindVarDropEq', which drops the residual equality permission
+  let e = PExpr_Unit in
+  implApplyImpl1 (Impl1_LetBind UnitRepr e)
+    (MNil :>: Impl1Cont (\(_ :>: n) -> pure n)) >>>= \n ->
+  -- Drop the n:eq(unit) permission
+  implDropM n (ValPerm_Eq e) >>>
+  pure n
+
+
 -- | Freshen up a sequence of names by replacing any duplicate names in the list
 -- with fresh, let-bound variables
 implFreshenNames :: NuMatchingAny1 r => RAssign ExprVar tps ->
@@ -3499,7 +3721,7 @@ implElimStructField x ps memb =
   let tp = RL.get memb (assignToRList tps) in
   implApplyImpl1 (Impl1_ElimStructField x ps tp memb)
   (MNil :>: Impl1Cont (\(_ :>: n) -> pure n)) >>>= \y ->
-  implPopM y (RL.get memb ps) >>>
+  recombinePerm y (RL.get memb ps) >>>
   pure y
 
 -- | Apply 'implElimStructField' to a sequence of fields in a struct permission,
@@ -3569,7 +3791,7 @@ implElimLLVMFieldContentsM _ fp
 implElimLLVMFieldContentsM x fp =
   implApplyImpl1 (Impl1_ElimLLVMFieldContents x fp)
   (MNil :>: Impl1Cont (\(_ :>: n) -> pure n)) >>>= \y ->
-  implPopM y (llvmFieldContents fp) >>>
+  recombinePerm y (llvmFieldContents fp) >>>
   pure y
 
 -- | Prove a reachability permission @x:P<args,e>@ from a proof of @x:eq(e)@ on
@@ -3619,7 +3841,7 @@ implElimLLVMBlockToEq _ (LLVMBlockPerm
 implElimLLVMBlockToEq x bp =
   implApplyImpl1 (Impl1_ElimLLVMBlockToEq x bp)
   (MNil :>: Impl1Cont (\(_ :>: n) -> pure n)) >>>= \y ->
-  implPopM y (ValPerm_Conj1 $ Perm_LLVMBlockShape $ modalizeBlockShape bp) >>>
+  recombinePerm y (ValPerm_Conj1 $ Perm_LLVMBlockShape $ modalizeBlockShape bp) >>>
   pure y
 
 -- | Try to prove a proposition about bitvectors dynamically, failing as in
@@ -3648,6 +3870,12 @@ implDropM :: HasCallStack => NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
              ImplM vars s r ps (ps :> a) ()
 implDropM x p = implSimplM Proxy (SImpl_Drop x p)
 
+-- | Drop zero or more permissions from the top of the stack
+implDropMultiM :: HasCallStack => NuMatchingAny1 r => DistPerms ps' ->
+                  ImplM vars s r ps (ps :++: ps') ()
+implDropMultiM MNil = return ()
+implDropMultiM (ps :>: VarAndPerm x p) = implDropM x p >>> implDropMultiM ps
+
 -- | Copy a permission on the top of the stack, assuming it is copyable
 implCopyM :: HasCallStack => NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
              ImplM vars s r (ps :> a :> a) (ps :> a) ()
@@ -3657,7 +3885,9 @@ implCopyM x p = implSimplM Proxy (SImpl_Copy x p)
 -- then pop it back to the variable permission for @x@
 implPushCopyM :: HasCallStack => NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
                  ImplM vars s r (ps :> a) ps ()
-implPushCopyM x p = implPushM x p >>> implCopyM x p >>> implPopM x p
+implPushCopyM x p =
+  implPushM x p >>> implCopyM x p >>> implPopM x p -- NOTE: must be implPopM and
+                                                   -- not recombinePerm
 
 -- | Swap the top two permissions on the top of the stack
 implSwapM :: HasCallStack => NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
@@ -3690,6 +3920,24 @@ implMoveUpM (ps :: prx ps) ps1 (x :: ExprVar a) ps2 =
         implSimplM (Proxy :: Proxy ps) (SImpl_MoveUp perms1 x p perms2)
     (DistPermsCons _ _x' _, _) -> error "implMoveUpM: unexpected variable"
 
+reflU :: () :~: ()
+reflU = Refl
+
+-- | Same as 'implMoveUpM' except the type lists are associated differently
+implMoveUpM' ::
+  NuMatchingAny1 r =>
+  prx ps -> RAssign f ps1 -> ExprVar a -> RAssign f ps2 ->
+  ImplM vars s r ((ps :++: ps1) :++: (RNil :> a :++: ps2))
+                 ((ps :> a :++: ps1) :++: ps2) ()
+implMoveUpM' (ps :: prx ps) (ps1 :: RAssign f ps1) (x :: ExprVar a)
+             (ps2 :: RAssign f ps2)
+  -- FIXME: build these proofs instead of just coercing them
+  | Refl <- unsafeCoerce reflU ::
+      ((ps :++: ps1) :++: (RNil :> a :++: ps2)) :~: (ps :++: ps1 :> a :++: ps2)
+  , Refl <- (unsafeCoerce reflU) ::
+      ((ps :> a :++: ps1) :++: ps2) :~: (ps :> a :++: ps1 :++: ps2) =
+    implMoveUpM ps ps1 x ps2
+
 -- | Move permission @p@ that is on the stack between two lists @ps1@ and @ps2@
 -- towards the bottom of the stack by moving it below both @ps1@ and @ps2@. That
 -- is, change the stack
@@ -3715,6 +3963,21 @@ implMoveDownM (ps :: prx ps) ps1x (x :: ExprVar a) ps2 =
         implSimplM (Proxy :: Proxy ps) (SImpl_MoveDown perms1 x p perms2)
     _ -> error "implMoveDownM: unexpected variable"
 
+-- | Same as 'implMoveDownM' except the type lists are associated differently
+implMoveDownM' ::
+  NuMatchingAny1 r =>
+  prx ps -> RAssign f (ps1 :> a) -> ExprVar a -> RAssign f ps2 ->
+  ImplM vars s r ((ps :> a :++: ps1) :++: ps2)
+                 ((ps :++: ps1) :++: (RNil :> a :++: ps2)) ()
+implMoveDownM' (ps :: prx ps) (ps1x :: RAssign f (ps1 :> a)) (x :: ExprVar a)
+               (ps2 :: RAssign f ps2)
+  -- FIXME: build these proofs instead of just coercing them
+  | Refl <- unsafeCoerce reflU ::
+      ((ps :> a :++: ps1) :++: ps2) :~: (ps :> a :++: ps1 :++: ps2)
+  , Refl <- unsafeCoerce reflU ::
+      ((ps :++: ps1) :++: (RNil :> a :++: ps2)) :~: (ps :++: ps1 :> a :++: ps2)
+  = implMoveDownM ps ps1x x ps2
+
 -- | Eliminate disjunctives and existentials on the top of the stack and return
 -- the resulting permission
 elimOrsExistsM :: NuMatchingAny1 r => ExprVar a ->
@@ -3807,6 +4070,13 @@ invTransEqM :: NuMatchingAny1 r => ExprVar a -> ExprVar a -> PermExpr a ->
                ImplM vars s r (ps :> a) (ps :> a :> a) ()
 invTransEqM x y e = implSimplM Proxy (SImpl_InvTransEq x y e)
 
+
+-- | For a unit variable @x@ and a unit-typed epxression @e@, prove @x:eq(e)@
+unitEqM :: NuMatchingAny1 r => ExprVar UnitType -> PermExpr UnitType ->
+           ImplM vars s r (ps :> UnitType) ps ()
+unitEqM x e = implSimplM Proxy (SImpl_UnitEq x e)
+
+
 -- | Copy an @x:eq(e)@ permission on the top of the stack
 introEqCopyM :: NuMatchingAny1 r => ExprVar a -> PermExpr a ->
                 ImplM vars s r (ps :> a :> a) (ps :> a) ()
@@ -3833,7 +4103,7 @@ introCastM x y p = implSimplM Proxy (SImpl_Cast x y p)
 -- it is not. It is an error if any of the supplied perms are not equality
 -- perms, or if any @xi@ does not have permission @eq(ei)@ in the current
 -- permission set for @ei@ not equal to @xi@.
-implProveEqPerms :: NuMatchingAny1 r => DistPerms ps' ->
+implProveEqPerms :: NuMatchingAny1 r => HasCallStack => DistPerms ps' ->
                     ImplM vars s r (ps :++: (RNil :> a :++: ps')) (ps :> a) ()
 implProveEqPerms DistPermsNil = pure ()
 implProveEqPerms (DistPermsCons ps' x (ValPerm_Eq (PExpr_Var y)))
@@ -3847,35 +4117,42 @@ implProveEqPerms (DistPermsCons ps' x p@(ValPerm_Eq _)) =
 implProveEqPerms _ = error "implProveEqPerms: non-equality permission"
 
 -- | Cast a proof of @x:p@ to one of @x:p'@ using a proof that @p=p'@
-implCastPermM :: HasCallStack => NuMatchingAny1 r => ExprVar a ->
-                 SomeEqProof (ValuePerm a) ->
+implCastPermM :: HasCallStack => NuMatchingAny1 r =>
+                 Proxy ps -> ExprVar a -> SomeEqProof (ValuePerm a) ->
                  ImplM vars s r (ps :> a) (ps :> a) ()
-implCastPermM x some_eqp
-  | UnSomeEqProof eqp <- unSomeEqProof some_eqp =
+implCastPermM ps x some_eqp
+  | UnSomeEqProof eqp <- unSomeEqProof some_eqp
+  , Refl <- RL.appendAssoc ps (MNil :>: eqProofLHS eqp) (eqProofPerms eqp) =
     implProveEqPerms (eqProofPerms eqp) >>>
-    implSimplM Proxy (SImpl_CastPerm x eqp)
+    implSimplM ps (SImpl_CastPerm x eqp) >>>
+    implDropMultiM (eqProofPerms eqp)
+
+distPermsProxy :: DistPerms ps -> Proxy ps
+distPermsProxy _ = Proxy
 
 -- | Cast a permission somewhere in the stack using an equality proof
 implCastStackElemM :: HasCallStack => NuMatchingAny1 r => Member ps a ->
-                      SomeEqProof (ValuePerm a) -> ImplM vars s r ps ps ()
-implCastStackElemM memb some_eqp =
+                      EqProof ps' (ValuePerm a) ->
+                      ImplM vars s r (ps :++: ps') (ps :++: ps') ()
+implCastStackElemM memb eqp =
+  let ps' = eqProofPerms eqp in
   getDistPerms >>>= \all_perms ->
-  case RL.memberSplitAt all_perms memb of
+  let ps = fst $ RL.split Proxy ps' all_perms in
+  case RL.memberSplitAt ps memb of
     RL.SplitAtMemberRet ps0 px@(VarAndPerm x _) ps1 ->
-      implMoveUpM ps0 ps1 x MNil >>>
-      implCastPermM x some_eqp >>>
-      implMoveDownM ps0 (ps1 :>: px) x MNil
+      implMoveUpM' ps0 ps1 x ps' >>>
+      implSimplM (distPermsProxy $ RL.append ps0 ps1) (SImpl_CastPerm x eqp) >>>
+      implMoveDownM' ps0 (ps1 :>: px) x ps'
 
 -- | Cast all of the permissions on the stack using 'implCastPermM'
 implCastStackM :: HasCallStack => NuMatchingAny1 r =>
-                  SomeEqProof (ValuePerms ps) ->
-                  ImplM vars s r ps ps ()
-implCastStackM some_eqp =
-  getDistPerms >>>= \perms ->
+                  EqProof ps' (ValuePerms ps) ->
+                  ImplM vars s r ps (ps :++: ps') ()
+implCastStackM eqp =
   RL.foldr (\memb m ->
-             implCastStackElemM memb (fmap (RL.get memb) some_eqp) >>> m)
-  (pure ())
-  (RL.members perms)
+             implCastStackElemM memb (fmap (RL.get memb) eqp) >>> m)
+  (implDropMultiM (eqProofPerms eqp))
+  (RL.members $ eqProofLHS eqp)
 
 -- | Introduce a proof of @x:true@ onto the top of the stack, which is the same
 -- as an empty conjunction
@@ -4109,7 +4386,7 @@ implBeginLifetimeM :: NuMatchingAny1 r =>
 implBeginLifetimeM =
   implApplyImpl1 Impl1_BeginLifetime
     (MNil :>: Impl1Cont (\(_ :>: n) -> pure n)) >>>= \l ->
-  implPopM l (ValPerm_LOwned [] MNil MNil) >>>
+  recombinePerm l (ValPerm_LOwned [] MNil MNil) >>>
   implTraceM (\i -> pretty "Beginning lifetime:" <+> permPretty i l) >>>
   pure l
 
@@ -4142,7 +4419,7 @@ implDropLifetimeConjsM l x ps
     implExtractSwapConjM x ps i >>>
     implDropM x (ValPerm_Conj1 (ps!!i)) >>>
     let ps' = deleteNth i ps in
-    implPopM x (ValPerm_Conj ps') >>>
+    recombinePerm x (ValPerm_Conj ps') >>>
     implDropLifetimeConjsM l x ps'
 implDropLifetimeConjsM _ _ _ = return ()
 
@@ -4178,7 +4455,7 @@ implSplitLifetimeM x f args l l2 sub_ls ps_in ps_out =
                     permPretty i x <> colon <>
                     permPretty i (ltFuncMinApply f l)]) >>>
   implSimplM Proxy (SImpl_SplitLifetime x f args l l2 sub_ls ps_in ps_out) >>>
-  getTopDistPerm l2 >>>= implPopM l2
+  getTopDistPerm l2 >>>= recombinePerm l2
 
 
 -- | Subsume a smaller lifetime @l2@ inside a bigger lifetime @l1@, by adding
@@ -4209,7 +4486,7 @@ implContainedLifetimeCurrentM :: NuMatchingAny1 r => ExprVar LifetimeType ->
                                  (ps :> LifetimeType) ()
 implContainedLifetimeCurrentM l ls ps_in ps_out l2 =
   implSimplM Proxy (SImpl_ContainedLifetimeCurrent l ls ps_in ps_out l2) >>>
-  implPopM l (ValPerm_LOwned ls ps_in ps_out)
+  recombinePerm l (ValPerm_LOwned ls ps_in ps_out)
 
 
 -- | Remove a finshed contained lifetime from an @lowned@ permission. Assume the
@@ -4228,7 +4505,7 @@ implRemoveContainedLifetimeM :: NuMatchingAny1 r => ExprVar LifetimeType ->
                                 (ps :> LifetimeType :> LifetimeType) ()
 implRemoveContainedLifetimeM l ls ps_in ps_out l2 =
   implSimplM Proxy (SImpl_RemoveContainedLifetime l ls ps_in ps_out l2) >>>
-  implPopM l (ValPerm_LOwned (delete (PExpr_Var l2) ls) ps_in ps_out)
+  recombinePerm l (ValPerm_LOwned (delete (PExpr_Var l2) ls) ps_in ps_out)
 
 
 -- | Find all lifetimes that we currently own which could, if ended, help prove
@@ -4285,7 +4562,7 @@ implLLVMFieldTryProveWordEq x fp =
     substEqsWithProof e >>>= \eqp ->
     case someEqProofRHS eqp of
       PExpr_LLVMWord e' ->
-        implCastPermM y (fmap ValPerm_Eq eqp) >>>
+        implCastPermM Proxy y (fmap ValPerm_Eq eqp) >>>
         let fp' = llvmFieldSetEqWord fp e' in
         introLLVMFieldContentsM x y fp' >>>
         return (Just e')
@@ -4358,7 +4635,7 @@ implLLVMFieldSplit x fp sz_bytes
         \(_ :>: VarAndPerm _ (ValPerm_Conj1 p1) :>:
           VarAndPerm _ (ValPerm_Conj1 p2) :>:
           VarAndPerm y p_y :>: VarAndPerm z p_z) ->
-        implPopM z p_z >>> implPopM y p_y >>> return (p1,p2)
+        recombinePerm z p_z >>> recombinePerm y p_y >>> return (p1,p2)
       Nothing ->
         implSimplM Proxy (SImpl_SplitLLVMTrueField x
                           (llvmFieldSetTrue fp fp) sz fp_m_sz) >>>
@@ -4394,7 +4671,7 @@ implLLVMFieldTruncate x fp sz'
         (MNil :>: Impl1Cont (const $ return ())) >>>
         getDistPerms >>>=
         \(_ :>: VarAndPerm _ (ValPerm_Conj1 p) :>: VarAndPerm y p_y) ->
-        implPopM y p_y >>> return p
+        recombinePerm y p_y >>> return p
       Nothing ->
         implSimplM Proxy (SImpl_TruncateLLVMTrueField x
                           (llvmFieldSetTrue fp fp) sz') >>>
@@ -4427,7 +4704,7 @@ implLLVMFieldConcat x fp1 fp2
         (Impl1_ConcatLLVMWordFields x (llvmFieldSetEqWord fp1 e1) e2 endianness)
         (MNil :>: Impl1Cont (const $ return ())) >>>
         getDistPerms >>>= \(_ :>: VarAndPerm y p_y) ->
-        implPopM y p_y
+        recombinePerm y p_y
       Nothing ->
         implSimplM Proxy (SImpl_ConcatLLVMTrueFields x
                           (llvmFieldSetTrue fp1 fp1)
@@ -4763,7 +5040,7 @@ implElimPopIthLLVMBlock :: (1 <= w, KnownNat w, NuMatchingAny1 r) =>
                            ImplM vars s r ps (ps :> LLVMPointerType w) ()
 implElimPopIthLLVMBlock x ps i
   | Perm_LLVMBlock bp <- ps!!i =
-    implExtractConjM x ps i >>> implPopM x (ValPerm_Conj $ deleteNth i ps) >>>
+    implExtractConjM x ps i >>> recombinePerm x (ValPerm_Conj $ deleteNth i ps) >>>
     implElimLLVMBlock x bp >>> getTopDistPerm x >>>= \p' -> recombinePerm x p'
 implElimPopIthLLVMBlock _ _ _ = error "implElimPopIthLLVMBlock: malformed inputs"
 
@@ -4970,7 +5247,7 @@ proveLifetimeCurrent (CurrentTransPerms cur_perms l) =
 -- | Simplify an equality permission @x:eq(e)@ that we assume is on the top of
 -- the stack by substituting any equality permissions on variables in @e@,
 -- returning the resulting expression
-simplEqPerm :: NuMatchingAny1 r => ExprVar a -> PermExpr a ->
+simplEqPerm :: HasCallStack => NuMatchingAny1 r => ExprVar a -> PermExpr a ->
                ImplM vars s r (as :> a) (as :> a) (PermExpr a)
 simplEqPerm x e@(PExpr_Var y) =
   getPerm y >>= \case
@@ -4985,26 +5262,24 @@ simplEqPerm _ e = pure e
 
 -- | Recombine the permission @x:p@ on top of the stack back into the existing
 -- permission for @x@
-recombinePerm :: NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
+recombinePerm :: HasCallStack => NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
                  ImplM vars s r as (as :> a) ()
 recombinePerm x p = getPerm x >>>= \x_p -> recombinePermExpl x x_p p
 
 -- | Recombine the permission @x:p@ on top of the stack back into the existing
 -- permission @x_p@ for @x@, where @x_p@ is given explicitly as the first
 -- permission argument and @p@ is the second
-recombinePermExpl :: NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
+recombinePermExpl :: HasCallStack => NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
                      ValuePerm a -> ImplM vars s r as (as :> a) ()
 recombinePermExpl x x_p p =
-  {-
-  use implStatePPInfo >>>= \info ->
-  tracePretty (string "recombinePerm" <+> permPretty info x
-               </> permPretty info x_p </> string "<-"
-               </> permPretty info p) $ -}
+  -- implTraceM (\i -> pretty "recombinePerm" <+> permPretty i x
+  --              <+> permPretty i x_p <+> pretty "<-"
+  --              <+> permPretty i p) >>>
   recombinePerm' x x_p p
 
 -- | This is the implementation of 'recombinePermExpl'; see the documentation
 -- for that function for details
-recombinePerm' :: NuMatchingAny1 r => ExprVar a -> ValuePerm a -> ValuePerm a ->
+recombinePerm' :: HasCallStack => NuMatchingAny1 r => ExprVar a -> ValuePerm a -> ValuePerm a ->
                   ImplM vars s r as (as :> a) ()
 recombinePerm' x _ p@ValPerm_True = implDropM x p
 recombinePerm' x _ ValPerm_False = implElimFalseM x
@@ -5028,6 +5303,9 @@ recombinePerm' x x_p@(ValPerm_Eq (PExpr_LLVMOffset y off)) (ValPerm_Conj ps) =
   castLLVMPtrM x (ValPerm_Conj ps) (bvNegate off) y >>>
   getPerm y >>>= \y_p ->
   recombinePermExpl y y_p (ValPerm_Conj $ mapMaybe (offsetLLVMAtomicPerm off) ps)
+recombinePerm' x _p p'@(ValPerm_Eq PExpr_Unit) =
+  -- When trying to combine a permission x:eq(()), just drop this permission
+  implDropM x p'
 recombinePerm' x p p'@(ValPerm_Eq _) =
   -- NOTE: we could handle this by swapping the stack with the variable perm and
   -- calling recombinePerm again, but this could potentially create permission
@@ -5063,7 +5341,7 @@ recombinePerm' x _ p = implDropM x p
 -- | Recombine a single conjuct @x:p@ on top of the stack back into the existing
 -- conjuctive permission @x_p1 * ... * x_pn@ for @x@, returning the resulting
 -- permission conjucts for @x@
-recombinePermConj :: NuMatchingAny1 r => ExprVar a -> [AtomicPerm a] ->
+recombinePermConj :: HasCallStack => NuMatchingAny1 r => ExprVar a -> [AtomicPerm a] ->
                      AtomicPerm a -> ImplM vars s r as (as :> a) ()
 
 -- If p is a field permission whose range is a subset of that of a permission we
@@ -5145,13 +5423,13 @@ recombinePermConj x x_ps p =
 
 
 -- | Recombine the permissions on the stack back into the permission set
-recombinePerms :: NuMatchingAny1 r => DistPerms ps -> ImplM vars s r RNil ps ()
+recombinePerms :: HasCallStack => NuMatchingAny1 r => DistPerms ps -> ImplM vars s r RNil ps ()
 recombinePerms DistPermsNil = pure ()
 recombinePerms (DistPermsCons ps' x p) =
   recombinePerm x p >>> recombinePerms ps'
 
 -- | Recombine some of the permissions on the stack back into the permission set
-recombinePermsPartial :: NuMatchingAny1 r => f ps -> DistPerms ps' ->
+recombinePermsPartial :: HasCallStack => NuMatchingAny1 r => f ps -> DistPerms ps' ->
                          ImplM vars s r ps (ps :++: ps') ()
 recombinePermsPartial _ DistPermsNil = pure ()
 recombinePermsPartial ps (DistPermsCons ps' x p) =
@@ -5159,7 +5437,7 @@ recombinePermsPartial ps (DistPermsCons ps' x p) =
 
 -- | Recombine some of the permissions on the stack back into the permission
 -- set, but in reverse order
-recombinePermsRevPartial :: NuMatchingAny1 r => RAssign Proxy ps1 -> DistPerms ps2 ->
+recombinePermsRevPartial :: HasCallStack => NuMatchingAny1 r => RAssign Proxy ps1 -> DistPerms ps2 ->
                             ImplM vars s r ps1 (ps1 :++: ps2) ()
 recombinePermsRevPartial _ DistPermsNil = return ()
 recombinePermsRevPartial ps1 ps2@(DistPermsCons ps2' x p) =
@@ -5169,13 +5447,13 @@ recombinePermsRevPartial ps1 ps2@(DistPermsCons ps2' x p) =
 
 -- | Recombine the permissions on the stack back into the permission set, but in
 -- reverse order
-recombinePermsRev :: NuMatchingAny1 r => DistPerms ps ->
+recombinePermsRev :: HasCallStack => NuMatchingAny1 r => DistPerms ps ->
                      ImplM vars s r RNil ps ()
 recombinePermsRev ps
   | Refl <- RL.prependRNilEq ps = recombinePermsRevPartial MNil ps
 
 -- | Recombine the permissions for a 'LifetimeCurrentPerms' list
-recombineLifetimeCurrentPerms :: NuMatchingAny1 r =>
+recombineLifetimeCurrentPerms :: HasCallStack => NuMatchingAny1 r =>
                                  LifetimeCurrentPerms ps_l ->
                                  ImplM vars s r ps (ps :++: ps_l) ()
 recombineLifetimeCurrentPerms AlwaysCurrentPerms = pure ()
@@ -5267,7 +5545,7 @@ substEqsWithProof a =
 
 
 -- | The main work horse for 'proveEq' on expressions
-proveEqH :: forall vars a s r ps. NuMatchingAny1 r =>
+proveEqH :: forall vars a s r ps. NuMatchingAny1 r => HasCallStack =>
             PartialSubst vars -> PermExpr a ->
             Mb vars (PermExpr a) ->
             ImplM vars s r ps ps (SomeEqProof (PermExpr a))
@@ -5278,6 +5556,7 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
   (_, [nuMP| PExpr_Var z |])
     | Left memb <- mbNameBoundP z
     , Nothing <- psubstLookup psubst memb ->
+      -- implTraceM (\i -> pretty "proveEqH (unset var):" <+> permPretty i e) >>>
       substEqsWithProof e >>= \eqp ->
       setVarM memb (someEqProofRHS eqp) >>> pure eqp
 
@@ -5285,16 +5564,20 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
   (_, [nuMP| PExpr_Var z |])
     | Left memb <- mbNameBoundP z
     , Just e' <- psubstLookup psubst memb ->
+      -- implTraceM (\i -> pretty "proveEqH (set var):" <+> permPretty i e) >>>
       proveEqH psubst e (mbConst e' z)
 
   -- If the RHS = LHS, do a proof by reflexivity
   _ | Just e' <- partialSubst psubst mb_e
-    , e == e' -> pure (SomeEqProofRefl e)
+    , e == e' ->
+      -- implTraceM (\i -> pretty "proveEqH (reflexivity):" <+> permPretty i e) >>>
+        pure (SomeEqProofRefl e)
 
   -- To prove x=y, try to see if either side has an eq permission, if necessary by
   -- eliminating compound permissions, and proceed by transitivity if possible
   (PExpr_Var x, [nuMP| PExpr_Var mb_y |])
     | Right y <- mbNameBoundP mb_y ->
+      -- implTraceM (\i -> pretty "proveEqH (left eq):" <+> permPretty i e) >>>
       getPerm x >>= \x_p ->
       getPerm y >>= \y_p ->
       case (x_p, y_p) of
@@ -5317,6 +5600,7 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
 
   -- To prove @x &+ o = e@, we subtract @o@ from the RHS and recurse
   (PExpr_LLVMOffset x off, _) ->
+    -- implTraceM (\i -> pretty "proveEqH (offsetL):" <+> permPretty i e) >>>
     proveEq (PExpr_Var x) (fmap (`addLLVMOffset` bvNegate off) mb_e) >>= \some_eqp ->
     pure $ fmap (`addLLVMOffset` off) some_eqp
 
@@ -5325,12 +5609,15 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
   (PExpr_Var x, [nuMP| PExpr_LLVMOffset mb_y mb_off |])
     | Right y <- mbNameBoundP mb_y
     , x == y ->
+      -- implTraceM (\i -> pretty "proveEqH (offsetR):" <+> permPretty i e) >>>
       proveEq (zeroOfType (BVRepr knownNat)) mb_off >>= \some_eqp ->
       pure $ someEqProofTrans (someEqProofZeroOffset y)
                               (fmap (PExpr_LLVMOffset y) some_eqp)
 
   -- To prove x=e, try to see if x:eq(e') and proceed by transitivity
   (PExpr_Var x, _) ->
+    -- implTraceM (\i -> pretty "proveEqH (x=e):" <+>
+    --                   permPretty i x <+> pretty "=" <+> permPretty i mb_e) >>>
     getVarEqPerm x >>= \case
     Just e' ->
       proveEq e' mb_e >>= \eqp2 ->
@@ -5340,6 +5627,8 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
   -- To prove e=x, try to see if x:eq(e') and proceed by transitivity
   (_, [nuMP| PExpr_Var z |])
     | Right x <- mbNameBoundP z ->
+    -- implTraceM (\i -> pretty "proveEqH (e=x):" <+>
+    --                   permPretty i e <+> pretty "=" <+> permPretty i x) >>>
       getVarEqPerm x >>= \case
         Just e' ->
           proveEq e (mbConst e' mb_e) >>= \eqp ->
@@ -5351,6 +5640,7 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
 
   -- Prove word(e1) = word(e2) by proving e1=e2
   (PExpr_LLVMWord e', [nuMP| PExpr_LLVMWord mb_e' |]) ->
+    -- implTraceM (\i -> pretty "proveEqH (word):" <+> permPretty i e) >>>
     fmap PExpr_LLVMWord <$> proveEqH psubst e' mb_e'
 
   -- Prove e = L_1*y_1 + ... + L_k*y_k + N*z + M where z is an unset variable,
@@ -5361,6 +5651,7 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
     | Just (n, memb, e_factors) <- getUnsetBVFactor psubst mb_factors
     , e' <- bvSub e (bvAdd e_factors (bvInt $ mbLift mb_m))
     , bvIsZero (bvMod e' n) ->
+    -- implTraceM (\i -> pretty "proveEqH (bv):" <+> permPretty i e) >>>
       setVarM memb (bvDiv e' n) >>> pure (SomeEqProofRefl e)
 
   -- FIXME: add cases to prove struct(es1)=struct(es2)
@@ -5369,14 +5660,21 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
   _ -> proveEqFail e mb_e
 
 
--- | Build a proof on the top of the stack that @x:eq(e)@. Assume that all @x@
--- permissions are on the top of the stack and given by argument @p@, and pop
--- them back to the primary permission for @x@ at the end of the proof.
-proveVarEq :: NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
-              Mb vars (PermExpr a) -> ImplM vars s r (ps :> a) (ps :> a) ()
-proveVarEq x p mb_e =
-  implPopM x p >>> proveEq (PExpr_Var x) mb_e >>>= \some_eqp ->
-  introEqReflM x >>> implCastPermM x (fmap ValPerm_Eq some_eqp)
+-- | Build a proof on the top of the stack that @x:eq(e)@
+proveVarEq :: NuMatchingAny1 r => ExprVar a -> Mb vars (PermExpr a) ->
+              ImplM vars s r (ps :> a) ps ()
+proveVarEq x mb_e =
+  proveEq (PExpr_Var x) mb_e >>>= \some_eqp ->
+  introEqReflM x >>> implCastPermM Proxy x (fmap ValPerm_Eq some_eqp)
+
+-- | Build proofs that @x1:eq(e1),...,xn:eq(en)@ on top of the stack
+proveVarsEq :: NuMatchingAny1 r => RAssign ExprVar as ->
+               Mb vars (RAssign PermExpr as) ->
+               ImplM vars s r (ps :++: as) ps ()
+proveVarsEq MNil _ = return ()
+proveVarsEq (xs' :>: x) es =
+  let [nuMP| es' :>: mb_e |] = mbMatch es in
+  proveVarsEq xs' es' >>> proveVarEq x mb_e
 
 -- | Prove that @e1=e2@ using 'proveEq' and then cast permission @x:(f e1)@,
 -- which is on top of the stack, to @x:(f e2)@
@@ -5385,7 +5683,7 @@ proveEqCast :: (ProveEq a, NuMatchingAny1 r) => ExprVar b ->
                ImplM vars s r (ps :> b) (ps :> b) ()
 proveEqCast x f e mb_e =
   do some_eqp <- proveEq e mb_e
-     implCastPermM x (fmap f some_eqp)
+     implCastPermM Proxy x (fmap f some_eqp)
 
 
 ----------------------------------------------------------------------
@@ -5910,7 +6208,7 @@ proveVarLLVMArrayH ::
 proveVarLLVMArrayH x _ psubst ps mb_ap
   | Just len <- partialSubst psubst $ mbLLVMArrayLen mb_ap
   , bvIsZero len =
-    implPopM x (ValPerm_Conj ps) >>>
+    recombinePerm x (ValPerm_Conj ps) >>>
     partialSubstForceM mb_ap "proveVarLLVMArray: incomplete psubst" >>>= \ap ->
     implLLVMArrayEmpty x ap
 
@@ -7168,7 +7466,7 @@ proveVarImplFoldRight x p mb_p = case mbMatch mb_p of
           RecursiveSortRepr _ _ -> implSetRecRecurseRightM
           _ -> pure ()) >>>
       implLookupNamedPerm npn >>>= \np ->
-      implPopM x p >>>
+      recombinePerm x p >>>
       -- FIXME: how to replace this mbMap2 with mbMapCl, to avoid refreshing all
       -- the names in mb_args and mb_off? Maybe they aren't that big anyway...
       proveVarImplInt x (mbMap2 (unfoldPerm np) mb_args mb_off) >>>
@@ -7201,6 +7499,7 @@ proveVarAtomicImplUnfoldOrFail x ps mb_ap =
 -- @true@. Any remaining perms for @x@ are popped off of the stack.
 proveVarAtomicImpl ::
   NuMatchingAny1 r =>
+  HasCallStack =>
   ExprVar a ->
   [AtomicPerm a] ->
   Mb vars (AtomicPerm a) ->
@@ -7219,46 +7518,46 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
                               Perm_LLVMFree e' -> Just e'
                               _ -> Nothing) ps of
       (i, e'):_ ->
-        implCopyConjM x ps i >>> implPopM x (ValPerm_Conj ps) >>>
+        implCopyConjM x ps i >>> recombinePerm x (ValPerm_Conj ps) >>>
         castLLVMFreeM x e' e
       _ -> proveVarAtomicImplUnfoldOrFail x ps mb_p
 
   [nuMP| Perm_LLVMFunPtr tp mb_p' |] ->
     partialSubstForceM mb_p' "proveVarAtomicImpl" >>>= \p ->
     case elemIndex (Perm_LLVMFunPtr (mbLift tp) p) ps of
-      Just i -> implCopyConjM x ps i >>> implPopM x (ValPerm_Conj ps)
+      Just i -> implCopyConjM x ps i >>> recombinePerm x (ValPerm_Conj ps)
       _ -> proveVarAtomicImplUnfoldOrFail x ps mb_p
 
   [nuMP| Perm_IsLLVMPtr |]
     | Just i <- elemIndex Perm_IsLLVMPtr ps ->
-      implCopyConjM x ps i >>> implPopM x (ValPerm_Conj ps)
+      implCopyConjM x ps i >>> recombinePerm x (ValPerm_Conj ps)
 
   [nuMP| Perm_IsLLVMPtr |]
     | Just i <- findIndex isLLVMFieldPerm ps
     , p@(Perm_LLVMField fp) <- ps !! i ->
-      implExtractConjM x ps i >>> implPopM x (ValPerm_Conj $ deleteNth i ps) >>>
+      implExtractConjM x ps i >>> recombinePerm x (ValPerm_Conj $ deleteNth i ps) >>>
       implSimplM Proxy (SImpl_LLVMFieldIsPtr x fp) >>>
       implPushM x (ValPerm_Conj $ deleteNth i ps) >>>
       implInsertConjM x p (deleteNth i ps) i >>>
-      implPopM x (ValPerm_Conj ps)
+      recombinePerm x (ValPerm_Conj ps)
 
   [nuMP| Perm_IsLLVMPtr |]
     | Just i <- findIndex isLLVMArrayPerm ps
     , p@(Perm_LLVMArray ap) <- ps !! i ->
-      implExtractConjM x ps i >>> implPopM x (ValPerm_Conj $ deleteNth i ps) >>>
+      implExtractConjM x ps i >>> recombinePerm x (ValPerm_Conj $ deleteNth i ps) >>>
       implSimplM Proxy (SImpl_LLVMArrayIsPtr x ap) >>>
       implPushM x (ValPerm_Conj $ deleteNth i ps) >>>
       implInsertConjM x p (deleteNth i ps) i >>>
-      implPopM x (ValPerm_Conj ps)
+      recombinePerm x (ValPerm_Conj ps)
 
   [nuMP| Perm_IsLLVMPtr |]
     | Just i <- findIndex isLLVMBlockPerm ps
     , p@(Perm_LLVMBlock bp) <- ps !! i ->
-      implExtractConjM x ps i >>> implPopM x (ValPerm_Conj $ deleteNth i ps) >>>
+      implExtractConjM x ps i >>> recombinePerm x (ValPerm_Conj $ deleteNth i ps) >>>
       implSimplM Proxy (SImpl_LLVMBlockIsPtr x bp) >>>
       implPushM x (ValPerm_Conj $ deleteNth i ps) >>>
       implInsertConjM x p (deleteNth i ps) i >>>
-      implPopM x (ValPerm_Conj ps)
+      recombinePerm x (ValPerm_Conj ps)
 
   [nuMP| Perm_IsLLVMPtr |] ->
     proveVarAtomicImplUnfoldOrFail x ps mb_p
@@ -7282,13 +7581,13 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
   [nuMP| Perm_LLVMFrame mb_fperms |]
     | [Perm_LLVMFrame fperms] <- ps ->
       proveEq fperms mb_fperms >>>= \eqp ->
-      implCastPermM x (fmap (ValPerm_Conj1 . Perm_LLVMFrame) eqp)
+      implCastPermM Proxy x (fmap (ValPerm_Conj1 . Perm_LLVMFrame) eqp)
 
   -- FIXME HERE: eventually we should handle lowned permissions on the right
   -- with arbitrary contained lifetimes, by equalizing the two sides
   [nuMP| Perm_LOwned [] _ _ |]
     | [Perm_LOwned (PExpr_Var l2:_) _ _] <- ps ->
-      implPopM x (ValPerm_Conj ps) >>> implEndLifetimeRecM l2 >>>
+      recombinePerm x (ValPerm_Conj ps) >>> implEndLifetimeRecM l2 >>>
       proveVarImplInt x (mbValPerm_Conj1 mb_p)
 
   [nuMP| Perm_LOwned [] mb_ps_inR mb_ps_outR |]
@@ -7341,7 +7640,7 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
     partialSubstForceM mb_l' "proveVarAtomicImpl" >>>= \l' ->
     case ps of
       _ | l' == PExpr_Var x ->
-          implPopM x (ValPerm_Conj ps) >>>
+          recombinePerm x (ValPerm_Conj ps) >>>
           implSimplM Proxy (SImpl_LCurrentRefl x)
       [Perm_LCurrent l] | l == l' -> pure ()
       [Perm_LCurrent (PExpr_Var l)] ->
@@ -7355,7 +7654,7 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
       _ -> proveVarAtomicImplUnfoldOrFail x ps mb_p
 
   [nuMP| Perm_LFinished |] ->
-    implPopM x (ValPerm_Conj ps) >>> implEndLifetimeRecM x >>>
+    recombinePerm x (ValPerm_Conj ps) >>> implEndLifetimeRecM x >>>
     implPushCopyM x ValPerm_LFinished
 
   -- If we have a struct permission on the left, eliminate it to a sequence of
@@ -7398,13 +7697,13 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
             case p of
               Perm_Fun fun_perm
                 | Just (Refl,Refl,Refl,Refl) <- funPermEq4 fun_perm fun_perm' ->
-                  implCopyConjM x ps i >>> implPopM x (ValPerm_Conj ps)
+                  implCopyConjM x ps i >>> recombinePerm x (ValPerm_Conj ps)
               _ -> rest)
     (proveVarAtomicImplUnfoldOrFail x ps mb_p)
     (zip [0..] ps)
 
   [nuMP| Perm_BVProp mb_prop |] ->
-    implPopM x (ValPerm_Conj ps) >>>
+    recombinePerm x (ValPerm_Conj ps) >>>
     partialSubstForceM mb_prop "proveVarAtomicImpl" >>>= \prop ->
     implTryProveBVProp x prop
 
@@ -7438,7 +7737,7 @@ proveVarConjImpl :: NuMatchingAny1 r => ExprVar a -> [AtomicPerm a] ->
 
 -- If we are done, we are done
 proveVarConjImpl x ps (mbMatch -> [nuMP| [] |]) =
-  implPopM x (ValPerm_Conj ps) >>> introConjM x
+  recombinePerm x (ValPerm_Conj ps) >>> introConjM x
 
 -- If there is a defined or recursive name on the right, prove it first,
 -- ensuring that we only choose recursive names if there are no defined ones,
@@ -7510,13 +7809,13 @@ proveVarImplH :: NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
 proveVarImplH x p mb_p = case (p, mbMatch mb_p) of
 
   -- Prove an empty conjunction trivially
-  (_, [nuMP| ValPerm_Conj [] |]) -> implPopM x p >>> introConjM x
+  (_, [nuMP| ValPerm_Conj [] |]) -> recombinePerm x p >>> introConjM x
 
   -- Prove x:eq(e) by calling proveVarEq; note that we do not eliminate
   -- disjunctive permissions first because some trivial equalities do not require
   -- any eq permissions on the left, and we do not eliminate equalities on the
   -- left first because that may be the equality we are trying to prove!
-  (_, [nuMP| ValPerm_Eq e |]) -> proveVarEq x p e
+  (_, [nuMP| ValPerm_Eq e |]) -> recombinePerm x p >>> proveVarEq x e
 
   -- Eliminate any disjunctions and existentials on the left
   (ValPerm_Or _ _, _) ->
@@ -7530,21 +7829,21 @@ proveVarImplH x p mb_p = case (p, mbMatch mb_p) of
   -- from x:eq(y) by first proving y:p and then casting
   (ValPerm_Eq (PExpr_Var y), _) ->
     introEqCopyM x (PExpr_Var y) >>>
-    implPopM x p >>>
+    recombinePerm x p >>>
     proveVarImplInt y mb_p >>>
     partialSubstForceM mb_p "proveVarImpl" >>>= \p' ->
     introCastM x y p'
 
   -- Prove x:eq(y &+ off) |- x:p by proving y:p@off and then casting
   (ValPerm_Eq e@(PExpr_LLVMOffset y off), _) ->
-      introEqCopyM x e >>> implPopM x p >>>
+      introEqCopyM x e >>> recombinePerm x p >>>
       proveVarImplInt y (fmap (offsetLLVMPerm off) mb_p) >>>
       partialSubstForceM mb_p "proveVarImpl" >>>= \p_r ->
       castLLVMPtrM y (offsetLLVMPerm off p_r) off x
 
   -- Prove x:(p1 \/ p2) by trying to prove x:p1 and x:p2 in two branches
   (_, [nuMP| ValPerm_Or mb_p1 mb_p2 |]) ->
-    implPopM x p >>>
+    recombinePerm x p >>>
     implCatchM "proveVarImplH" (ColonPair x mb_p)
     (proveVarImplInt x mb_p1 >>>
      partialSubstForceM mb_p1 "proveVarImpl" >>>= \p1 ->
@@ -7574,7 +7873,7 @@ proveVarImplH x p mb_p = case (p, mbMatch mb_p) of
       implCatchM "proveVarImplH" (ColonPair x mb_p)
 
       -- Reflexivity branch: pop x:P<...>, prove x:eq(e), and use reflexivity
-      (implPopM x p >>> proveVarImplInt x (mbValPerm_Eq mb_e2) >>>
+      (recombinePerm x p >>> proveVarImplInt x (mbValPerm_Eq mb_e2) >>>
        partialSubstForceM mb_args2 "proveVarImpl" >>>= \args2 ->
         implReachabilityReflM x npn args2 off)
 
@@ -7702,7 +8001,7 @@ proveVarImplH x p mb_p = case (p, mbMatch mb_p) of
   -- If x:eq(struct(e1,...,en)) then we eliminate to x:struct(eq(e1),...,eq(en))
   (ValPerm_Eq (PExpr_Struct exprs), [nuMP| ValPerm_Conj _ |]) ->
     implSimplM Proxy (SImpl_StructEqToPerm x exprs) >>>
-    implPopM x (ValPerm_Conj1 $ Perm_Struct $
+    recombinePerm x (ValPerm_Conj1 $ Perm_Struct $
                 RL.map ValPerm_Eq $ exprsToRAssign exprs) >>>
     proveVarImplInt x mb_p
 
@@ -7715,7 +8014,7 @@ proveVarImplH x p mb_p = case (p, mbMatch mb_p) of
         | [nuMP| Just (Refl,Refl,Refl, Refl) |] <-
             mbMatch $ fmap (funPermEq4 fun_perm) mb_fun_perm ->
           introEqCopyM x (PExpr_Fun f) >>>
-          implPopM x p >>>
+          recombinePerm x p >>>
           implSimplM Proxy (SImpl_ConstFunPerm x f fun_perm ident)
       _ -> implFailVarM "proveVarImplH" x p mb_p
 
@@ -8090,19 +8389,30 @@ proveVarsImplEVarExprs ps =
 proveVarsImplVarEVars :: NuMatchingAny1 r => ExDistPerms vars as ->
                          ImplM vars s r as RNil (RAssign ExprVar vars)
 proveVarsImplVarEVars mb_ps =
+  -- First, prove the required permissions mb_ps. Note that this will prove
+  -- [es/vars]mb_ps, for some instantiation es for the evars vars. The rest of
+  -- this function is then to cast this to [xs/vars]mb_ps for fresh vars xs.
   proveVarsImpl mb_ps >>>
+  -- Next, call getVarVarM to get fresh variables for all the evars
   use implStateVars >>>= \vars ->
-  -- gmodify (over implStatePSubst (completePSubst vars)) >>>
-  traverseRAssign getVarVarM (RL.members $ cruCtxProxies vars) >>>= \xs ->
+  let var_membs = RL.members $ cruCtxProxies vars in
+  traverseRAssign getVarVarM var_membs >>>= \xs ->
+  -- Now get the instantiations es for the evars; NOTE: we call completePSubst
+  -- as a convenience, but all evars should be set by getVarVarM
   getPSubst >>>= \psubst ->
-  let s = completePSubst vars psubst in
-  let vars_eqpf =
-        traverseRAssign (\(Pair x e) -> someEqProof1 x e False) $
-        RL.map2 Pair xs (exprsOfSubst s) in
-  let perms_eqpf = fmap (\es -> subst (substOfExprs es) $
-                                mbDistPermsToValuePerms mb_ps) vars_eqpf in
-  implCastStackM perms_eqpf >>>
-  pure xs
+  let s = completePSubst vars psubst
+      es = exprsOfSubst s
+      mb_es = fmap (const es) mb_ps in
+  -- Prove that x:eq(e) for each evar x and its instantiation e
+  proveVarsEq xs mb_es >>>
+  -- Build the proof that [es/vars]mb_ps = [xs/vars]mb_ps
+  let eqpf =
+        fmap (\es' -> subst (substOfExprs es') $
+                      mbDistPermsToValuePerms mb_ps) $
+        eqProofFromPermsRev xs es in
+  -- Use eqpf to cast the permission stack
+  implCastStackM eqpf >>>
+  return xs
 
 -- | Prove @x:p'@, where @p@ may have existentially-quantified variables in it.
 proveVarImpl :: NuMatchingAny1 r => ExprVar a -> Mb vars (ValuePerm a) ->
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index 40eea5033e..1d214983dc 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -376,6 +376,16 @@ instance (PermPretty a, PermPretty b, PermPretty c) => PermPretty (a,b,c) where
 instance PermPretty a => PermPretty [a] where
   permPrettyM as = ppEncList False <$> mapM permPrettyM as
 
+
+instance PermPretty a => PermPretty (Maybe a) where
+  permPrettyM Nothing = return $ pretty "Nothing"
+  permPrettyM (Just a) = do
+    a_pp <- permPrettyM a
+    return (pretty "Just" <+> a_pp)
+
+instance PermPrettyF f => PermPretty (Some f) where
+  permPrettyM (Some x) = permPrettyMF x
+
 instance PermPretty (ExprVar a) where
   permPrettyM x =
     do maybe_str <- NameMap.lookup x <$> ppExprNames <$> ask
@@ -393,6 +403,10 @@ instance PermPrettyF f => PermPretty (RAssign f ctx) where
   permPrettyM xs =
     ppCommaSep <$> sequence (RL.mapToList permPrettyMF xs)
 
+instance PermPrettyF f => PermPrettyF (RAssign f) where
+  permPrettyMF xs = permPrettyM xs
+
+
 instance PermPretty (TypeRepr a) where
   permPrettyM UnitRepr = return $ pretty "unit"
   permPrettyM BoolRepr = return $ pretty "bool"
@@ -5085,7 +5099,11 @@ permIsCopyable :: ValuePerm a -> Bool
 permIsCopyable (ValPerm_Eq _) = True
 permIsCopyable (ValPerm_Or p1 p2) = permIsCopyable p1 && permIsCopyable p2
 permIsCopyable (ValPerm_Exists mb_p) = mbLift $ fmap permIsCopyable mb_p
-permIsCopyable (ValPerm_Named npn args _) =
+permIsCopyable (ValPerm_Named npn args _offset) =
+  -- FIXME: this is wrong. For transparent perms, should make this just unfold
+  -- the definition; for opaque perms, look at arguments. For recursive perms,
+  -- unfold and assume the recursive call is copyable, then see if the unfolded
+  -- version is still copyable
   namedPermArgsAreCopyable (namedPermNameArgs npn) args
 permIsCopyable (ValPerm_Var _ _) = False
 permIsCopyable (ValPerm_Conj ps) = all atomicPermIsCopyable ps
@@ -5482,10 +5500,21 @@ instance NeededVars (PermExpr a) where
   -- FIXME: need a better explanation of why this is the right answer...
   neededVars e = if isDeterminingExpr e then NameSet.empty else freeVars e
 
+instance NeededVars (PermExprs args) where
+  neededVars PExprs_Nil = NameSet.empty
+  neededVars (PExprs_Cons es e) = NameSet.union (neededVars es) (neededVars e)
+
 instance NeededVars (ValuePerm a) where
   neededVars (ValPerm_Eq e) = neededVars e
   neededVars (ValPerm_Or p1 p2) = NameSet.union (neededVars p1) (neededVars p2)
   neededVars (ValPerm_Exists mb_p) = NameSet.liftNameSet $ fmap neededVars mb_p
+  neededVars (ValPerm_Named name args offset)
+    | OpaqueSortRepr _ <- namedPermNameSort name =
+      NameSet.union (neededVars args) (freeVars offset)
+  -- FIXME: for non-opaque named permissions, we currently define the
+  -- @neededVars@ as all free variables of @p@, but this is incorrect for
+  -- defined or recursive permissions that do determine their variable arguments
+  -- when unfolded.
   neededVars p@(ValPerm_Named _ _ _) = freeVars p
   neededVars p@(ValPerm_Var _ _) = freeVars p
   neededVars (ValPerm_Conj ps) = neededVars ps
@@ -7631,11 +7660,18 @@ varPermsTransFreeVars =
             (SomeRAssign ns', Some rest) ->
               Some $ append ns' rest
 
+
+-- | Initialize the primary permission of a variable to the given permission if
+-- the variable is not yet set
+initVarPermWith :: ExprVar a -> ValuePerm a -> PermSet ps -> PermSet ps
+initVarPermWith x p =
+  over varPermMap $ \nmap ->
+  if NameMap.member x nmap then nmap else NameMap.insert x p nmap
+
 -- | Initialize the primary permission of a variable to @true@ if it is not set
 initVarPerm :: ExprVar a -> PermSet ps -> PermSet ps
 initVarPerm x =
-  over varPermMap $ \nmap ->
-  if NameMap.member x nmap then nmap else NameMap.insert x ValPerm_True nmap
+  initVarPermWith x ValPerm_True
 
 -- | Set the primary permissions for a sequence of variables to @true@
 initVarPerms :: RAssign Name (as :: RList CrucibleType) -> PermSet ps ->
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index d77917b534..9e2f4edc6d 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -2318,18 +2318,16 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     (\(pctx :>: _ :>: ptrans) -> pctx :>: ptrans)
     m
 
-  [nuMP| SImpl_CastPerm (x::ExprVar a) eqp |] ->
-    do ttrans <- translateSimplImplOutHead mb_simpl
+  [nuMP| SImpl_CastPerm (_::ExprVar a) eqp |] ->
+    do ttrans <- translateSimplImplOut mb_simpl
        let prxs_a = MNil :>: (Proxy :: Proxy a)
        let prxs1 = mbLift $ mbMapCl $(mkClosed [| distPermsToProxies
                                                 . eqProofPerms |]) eqp
        let prxs = RL.append prxs_a prxs1
-       withPermStackM
-         (\vars -> fst (RL.split ps0 prxs vars) :>: translateVar x)
+       withPermStackM id
          (\pctx ->
-           let (pctx1, pctx2) = RL.split ps0 prxs pctx
-               (_ :>: ptrans, _) = RL.split prxs_a prxs1 pctx2 in
-           pctx1 :>: typeTransF ttrans (transTerms ptrans))
+           let (pctx1, pctx2) = RL.split ps0 prxs pctx in
+           RL.append pctx1 (typeTransF ttrans (transTerms pctx2)))
          m
 
   [nuMP| SImpl_IntroEqRefl x |] ->
@@ -2347,6 +2345,12 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
        withPermStackM RL.tail
          (\(pctx :>: _ :>: _) -> pctx :>: typeTransF ttrans []) m
 
+  [nuMP| SImpl_UnitEq x _ |] ->
+    do ttrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM (:>: translateVar x)
+         (\pctx -> pctx :>: typeTransF ttrans []) m
+
+
   [nuMP| SImpl_CopyEq _ _ |] ->
     withPermStackM
     (\(vars :>: var) -> (vars :>: var :>: var))
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
index 21116bbaca..e65b7a1e62 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
@@ -82,6 +82,8 @@ import Verifier.SAW.Heapster.Permissions
 import Verifier.SAW.Heapster.Widening
 
 
+import GHC.Stack (HasCallStack)
+
 ----------------------------------------------------------------------
 -- * Handling Crucible Extensions
 ----------------------------------------------------------------------
@@ -1862,6 +1864,9 @@ data PermCheckState ext blocks tops rets ps =
     stTopVars   :: !(RAssign Name tops),
     stCurEntry  :: !(Some (TypedEntryID blocks)),
     stVarTypes  :: !(NameMap TypeRepr),
+    stUnitVar   :: !(Maybe (ExprVar UnitType)),
+    -- ^ An optional global unit variable that all other unit variables will be
+    -- equal to
     stPPInfo    :: !PPInfo,
     stErrPrefix :: !(Maybe (Doc ())),
     stDebug     :: ![Maybe String]
@@ -1881,6 +1886,7 @@ emptyPermCheckState perms tops entryID names =
                    stTopVars   = tops,
                    stCurEntry  = Some entryID,
                    stVarTypes  = NameMap.empty,
+                   stUnitVar   = Nothing,
                    stPPInfo    = emptyPPInfo,
                    stErrPrefix = Nothing,
                    stDebug     = names }
@@ -1955,6 +1961,12 @@ setInputExtState ExtRepr_LLVM _ _ =
 -- | Run a 'PermCheckM' computation for a particular entrypoint with a given set
 -- of top-level arguments, local arguments, ghost variables, and permissions on
 -- all three, and return a result inside a binding for these variables
+--
+-- Note that calls to @runPermCheckM@ should be accompanied by calls to
+-- @handleUnitVars@ or @stmtHandleUnitVars@ to ensure that all unit-typed
+-- variables are unified during type-checking. These functions are not currently
+-- combined because @handleUnitVars@ embeds an @ImplM@ computation and someties
+-- it is more convenient to combine multiple @ImplM@ computations into one.
 runPermCheckM ::
   KnownRepr ExtRepr ext =>
   [Maybe String] ->
@@ -1962,8 +1974,10 @@ runPermCheckM ::
   CruCtx args -> CruCtx ghosts -> MbValuePerms ((tops :++: args) :++: ghosts) ->
   (RAssign ExprVar tops -> RAssign ExprVar args -> RAssign ExprVar ghosts ->
    DistPerms ((tops :++: args) :++: ghosts) ->
-   PermCheckM ext cblocks blocks tops rets () ps_out r ((tops :++: args)
-                                                        :++: ghosts) ()) ->
+   PermCheckM ext cblocks blocks tops rets
+              () ps_out
+              r ((tops :++: args) :++: ghosts)
+              ()) ->
   TopPermCheckM ext cblocks blocks tops rets (Mb ((tops :++: args) :++: ghosts) r)
 runPermCheckM names entryID args ghosts mb_perms_in m =
   get >>= \(TopPermCheckState {..}) ->
@@ -2230,24 +2244,43 @@ getVarTypes :: RAssign Name tps ->
 getVarTypes MNil = pure CruCtxNil
 getVarTypes (xs :>: x) = CruCtxCons <$> getVarTypes xs <*> getVarType x
 
+-- | Output a string representing a variable given optional information such as
+-- a base name and a C name
+dbgStringPP ::
+  Maybe String -> -- ^ The base name of the variable (e.g., "top", "arg", etc.)
+  Maybe String -> -- ^ The C name of the variable, if applicable
+  TypeRepr a -> -- ^ The type of the variable
+  String
+dbgStringPP _          (Just d) _  = "C[" ++ d ++ "]"
+dbgStringPP (Just str) _        tp = str ++ "_" ++ typeBaseName tp
+dbgStringPP Nothing    Nothing  tp = typeBaseName tp
+
+
+-- | After all variables have been added to the context, unify all unit-typed
+-- variables by lifting through the ImplM monad
+stmtHandleUnitVars :: forall (tps :: RList CrucibleType)
+                             ext cblocks blocks tops ret ps.
+                      PermCheckExtC ext =>
+                      RAssign Name tps ->
+                      StmtPermCheckM ext cblocks blocks tops ret ps ps ()
+stmtHandleUnitVars ns =
+    stmtEmbedImplM $ handleUnitVars ns
+
 -- | Remember the type of a free variable, and ensure that it has a permission
 setVarType ::
   Maybe String -> -- ^ The base name of the variable (e.g., "top", "arg", etc.)
   Maybe String -> -- ^ The C name of the variable, if applicable
-  ExprVar a -> -- ^ The Hobbits variable itself
-  TypeRepr a -> -- ^ The type of the variable
+  ExprVar a    -> -- ^ The Hobbits variable itself
+  TypeRepr a   -> -- ^ The type of the variable
   PermCheckM ext cblocks blocks tops rets r ps r ps ()
 setVarType maybe_str dbg x tp =
-  let str' =
-        case (maybe_str,dbg) of
-          (_,Just d) -> "C[" ++ d ++ "]"
-          (Just str,_) -> str ++ "_" ++ typeBaseName tp
-          (Nothing,Nothing) -> typeBaseName tp
-  in
-  modify $ \st ->
-  st { stCurPerms = initVarPerm x (stCurPerms st),
-       stVarTypes = NameMap.insert x tp (stVarTypes st),
-       stPPInfo = ppInfoAddExprName str' x (stPPInfo st) }
+    (modify $ \st ->
+         st { stCurPerms = initVarPerm x (stCurPerms st),
+              stVarTypes = NameMap.insert x tp (stVarTypes st),
+              stPPInfo   = ppInfoAddExprName (dbgStringPP maybe_str dbg tp)
+                                             x
+                                            (stPPInfo st)
+         })
 
 -- | Remember the types of a sequence of free variables
 setVarTypes ::
@@ -2307,6 +2340,8 @@ localPermCheckM m =
 
 -- | Call 'runImplM' in the 'PermCheckM' monad
 pcmRunImplM ::
+  HasCallStack =>
+  NuMatchingAny1 r =>
   CruCtx vars -> Doc () -> (a -> r ps_out) ->
   ImplM vars (InnerPermCheckState blocks tops rets) r ps_out ps_in a ->
   PermCheckM ext cblocks blocks tops rets r' ps_in r' ps_in
@@ -2315,17 +2350,20 @@ pcmRunImplM vars fail_doc retF impl_m =
   getErrorPrefix >>>= \err_prefix ->
   (stPermEnv <$> top_get) >>>= \env ->
   gets stCurPerms >>>= \perms_in ->
-  gets stPPInfo   >>>= \ppInfo ->
+  gets stPPInfo   >>>= \ppInfo   ->
   gets stVarTypes >>>= \varTypes ->
+  gets stUnitVar  >>>= \unitVar  ->
   (stEndianness <$> top_get) >>>= \endianness ->
   (stDebugLevel <$> top_get) >>>= \dlevel ->
   liftPermCheckM $ lift $
   fmap (AnnotPermImpl (renderDoc (err_prefix <> line <> fail_doc))) $
-  runImplM vars perms_in env ppInfo "" dlevel varTypes endianness impl_m
+  runImplM vars perms_in env ppInfo "" dlevel varTypes unitVar endianness impl_m
   (return . retF . fst)
 
 -- | Call 'runImplImplM' in the 'PermCheckM' monad
 pcmRunImplImplM ::
+  HasCallStack =>
+  NuMatchingAny1 r =>
   CruCtx vars -> Doc () ->
   ImplM vars (InnerPermCheckState blocks tops rets) r ps_out ps_in (PermImpl
                                                                     r ps_out) ->
@@ -2337,15 +2375,18 @@ pcmRunImplImplM vars fail_doc impl_m =
   gets stCurPerms >>>= \perms_in ->
   gets stPPInfo   >>>= \ppInfo ->
   gets stVarTypes >>>= \varTypes ->
+  gets stUnitVar  >>>= \unitVar ->
   (stEndianness <$> top_get) >>>= \endianness ->
   (stDebugLevel <$> top_get) >>>= \dlevel ->
   liftPermCheckM $ lift $
   fmap (AnnotPermImpl (renderDoc (err_prefix <> line <> fail_doc))) $
-  runImplImplM vars perms_in env ppInfo "" dlevel varTypes endianness impl_m
+  runImplImplM vars perms_in env ppInfo "" dlevel varTypes unitVar endianness impl_m
 
 -- | Embed an implication computation inside a permission-checking computation,
 -- also supplying an overall error message for failures
 pcmEmbedImplWithErrM ::
+  HasCallStack =>
+  NuMatchingAny1 r =>
   (forall ps. AnnotPermImpl r ps -> r ps) -> CruCtx vars -> Doc () ->
   ImplM vars (InnerPermCheckState blocks tops rets) r ps_out ps_in a ->
   PermCheckM ext cblocks blocks tops rets (r ps_out) ps_out (r ps_in) ps_in
@@ -2356,22 +2397,27 @@ pcmEmbedImplWithErrM f_impl vars fail_doc m =
                                     (err_prefix <> line <> fail_doc))) <$>) >>>
   (stPermEnv  <$> top_get) >>>= \env ->
   gets stCurPerms >>>= \perms_in ->
-  gets stPPInfo   >>>= \ppInfo ->
+  gets stPPInfo   >>>= \ppInfo   ->
   gets stVarTypes >>>= \varTypes ->
+  gets stUnitVar  >>>= \unitVar  ->
   (stEndianness <$> top_get) >>>= \endianness ->
   (stDebugLevel <$> top_get) >>>= \dlevel ->
 
-  addReader (gcaptureCC
-             (runImplM vars perms_in env ppInfo "" dlevel varTypes endianness m))
+  addReader
+    (gcaptureCC
+      (runImplM vars perms_in env ppInfo "" dlevel varTypes unitVar endianness m))
     >>>= \(a, implSt) ->
 
-  gmodify ((\st -> st { stPPInfo = implSt ^. implStatePPInfo,
-                        stVarTypes = implSt ^. implStateNameTypes })
+  gmodify ((\st -> st { stPPInfo   = implSt ^. implStatePPInfo,
+                        stVarTypes = implSt ^. implStateNameTypes,
+                        stUnitVar  = implSt ^. implStateUnitVar })
            . setSTCurPerms (implSt ^. implStatePerms)) >>>
   pure (completePSubst vars (implSt ^. implStatePSubst), a)
 
 -- | Embed an implication computation inside a permission-checking computation
 pcmEmbedImplM ::
+  HasCallStack =>
+  NuMatchingAny1 r =>
   (forall ps. AnnotPermImpl r ps -> r ps) -> CruCtx vars ->
   ImplM vars (InnerPermCheckState blocks tops rets) r ps_out ps_in a ->
   PermCheckM ext cblocks blocks tops rets (r ps_out) ps_out (r ps_in) ps_in
@@ -2381,6 +2427,8 @@ pcmEmbedImplM f_impl vars m = pcmEmbedImplWithErrM f_impl vars mempty m
 -- | Special case of 'pcmEmbedImplM' for a statement type-checking context where
 -- @vars@ is empty
 stmtEmbedImplM ::
+  HasCallStack =>
+  NuMatchingExtC ext =>
   ImplM RNil (InnerPermCheckState
               blocks tops rets) (TypedStmtSeq ext blocks tops rets) ps_out ps_in a ->
   StmtPermCheckM ext cblocks blocks tops rets ps_out ps_in a
@@ -2389,7 +2437,9 @@ stmtEmbedImplM m = snd <$> pcmEmbedImplM TypedImplStmt emptyCruCtx m
 -- | Recombine any outstanding distinguished permissions back into the main
 -- permission set, in the context of type-checking statements
 stmtRecombinePerms ::
-  PermCheckExtC ext => StmtPermCheckM ext cblocks blocks tops rets RNil ps_in ()
+  HasCallStack =>
+  PermCheckExtC ext =>
+  StmtPermCheckM ext cblocks blocks tops rets RNil ps_in ()
 stmtRecombinePerms =
   get >>>= \(!st) ->
   let dist_perms = view distPerms (stCurPerms st) in
@@ -2584,6 +2634,7 @@ extractBVBytes loc sz off_bytes (reg :: TypedReg (BVType w)) =
 -- freshly-bound names for the return values. Return those freshly-bound names
 -- for the return values.
 emitStmt ::
+  PermCheckExtC ext =>
   CruCtx stmt_rets ->
   RAssign (Constant (Maybe String)) stmt_rets ->
   ProgramLoc ->
@@ -2596,6 +2647,8 @@ emitStmt tps names loc stmt =
     (mbPure (cruCtxProxies tps) ()) >>>= \(ns, ()) ->
   setVarTypes Nothing names ns tps >>>
   gmodify (modifySTCurPerms (applyTypedStmt stmt ns)) >>>
+  -- Note: must come after both setVarTypes and gmodify
+  stmtHandleUnitVars ns >>>
   pure ns
 
 
@@ -3331,7 +3384,8 @@ tcEmitLLVMStmt arch ctx loc (LLVM_MemClear _ (ptr :: Reg ctx (LLVMPointerType wp
       Perm_LLVMField fp ->
         stmtProvePerm tptr (emptyMb $ ValPerm_Conj1 $ Perm_LLVMField fp) >>>
         emitTypedLLVMStore arch Nothing loc tptr fp (PExpr_LLVMWord (bvInt 0)) DistPermsNil >>>
-        stmtRecombinePerms
+        stmtRecombinePerms >>>
+        pure ()
       _ -> error "Unexpected return value from llvmFieldsOfSize") >>>
 
   -- Return a fresh unit variable
@@ -3659,7 +3713,7 @@ castUnDetVarsForVar det_vars x =
         NameMap.assocs var_perm_map in
   let eqp = someEqProofFromSubst nondet_perms p in
   implPushM x p >>>
-  implCastPermM x eqp >>>
+  implCastPermM Proxy x eqp >>>
   implPopM x (someEqProofRHS eqp)
 
 -- | Simplify and drop permissions @p@ on variable @x@ so they only depend on
@@ -4038,6 +4092,8 @@ tcBlockEntryBody names blk entry@(TypedEntry {..}) =
                <> line <>
                pretty "Input perms:"
                <> align (permPretty i perms)) >>>
+  -- handle unit variables
+  stmtHandleUnitVars ns >>>
   stmtRecombinePerms >>>
   tcEmitStmtSeq names ctx (blk ^. blockStmts)
 
@@ -4056,9 +4112,10 @@ proveCallSiteImpl ::
 proveCallSiteImpl srcID destID args ghosts vars mb_perms_in mb_perms_out =
   fmap CallSiteImpl $ runPermCheckM [] srcID args vars mb_perms_in $
   \tops_ns args_ns _ perms_in ->
-  let perms_out =
+  let ns = RL.append tops_ns args_ns
+      perms_out =
         give (cruCtxProxies ghosts) $
-        varSubst (permVarSubstOfNames $ RL.append tops_ns args_ns) $
+        varSubst (permVarSubstOfNames $ ns) $
         mbSeparate (cruCtxProxies ghosts) $
         mbValuePermsToDistPerms mb_perms_out in
   stmtTraceM (\i ->
@@ -4071,8 +4128,11 @@ proveCallSiteImpl srcID destID args ghosts vars mb_perms_in mb_perms_out =
   -- FIXME HERE NOW: add the input perms and call site to our error message
   let err = ppProofError ppInfo perms_out in
   pcmRunImplM ghosts err
-  (CallSiteImplRet destID ghosts Refl (RL.append tops_ns args_ns))
-  (recombinePerms perms_in >>> proveVarsImplVarEVars perms_out) >>>= \impl ->
+    (CallSiteImplRet destID ghosts Refl ns)
+    (handleUnitVars ns >>>
+     recombinePerms perms_in >>>
+     proveVarsImplVarEVars perms_out
+     ) >>>= \impl ->
   gmapRet (>> return impl)