diff --git a/cabal.GHC-8.10.3.config b/cabal.GHC-8.10.3.config
index 42a1cc82cf..0ebe4cfe91 100644
--- a/cabal.GHC-8.10.3.config
+++ b/cabal.GHC-8.10.3.config
@@ -298,7 +298,7 @@ constraints: any.Cabal ==3.2.1.0,
              any.text-short ==0.1.3,
              text-short -asserts,
              any.tf-random ==0.5,
-             any.th-abstraction ==0.3.2.0,
+             any.th-abstraction ==0.4.2.0,
              any.th-compat ==0.1.1,
              any.th-expand-syns ==0.4.6.0,
              any.th-lift ==0.8.2,
diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config
index db72e5fd0f..f6733e8cf2 100644
--- a/cabal.GHC-8.8.4.config
+++ b/cabal.GHC-8.8.4.config
@@ -300,7 +300,7 @@ constraints: any.Cabal ==3.0.1.0,
              any.text-short ==0.1.3,
              text-short -asserts,
              any.tf-random ==0.5,
-             any.th-abstraction ==0.3.2.0,
+             any.th-abstraction ==0.4.2.0,
              any.th-compat ==0.1.1,
              any.th-expand-syns ==0.4.6.0,
              any.th-lift ==0.8.2,
diff --git a/cabal.project b/cabal.project
index 4a6af270cf..54107c9e98 100644
--- a/cabal.project
+++ b/cabal.project
@@ -43,4 +43,4 @@ packages:
 source-repository-package
     type: git
     location: https://github.com/eddywestbrook/hobbits.git
-    tag: e5918895396b6bcee2fc39f6bd0d77a90a52ba5f
+    tag: 20b6d18758312deaf6a544d474483e537d5f018f
diff --git a/heapster-saw/examples/rust_data.bc b/heapster-saw/examples/rust_data.bc
index 01d5a22c01..dd9d79894d 100644
Binary files a/heapster-saw/examples/rust_data.bc and b/heapster-saw/examples/rust_data.bc differ
diff --git a/heapster-saw/examples/rust_data.rs b/heapster-saw/examples/rust_data.rs
index 99ce465fa4..05fc52a5f1 100644
--- a/heapster-saw/examples/rust_data.rs
+++ b/heapster-saw/examples/rust_data.rs
@@ -315,3 +315,138 @@ pub fn tree_sum (t: &Tree<u64>) -> u64 {
     }
 }
 */
+
+/* A 20-element enum that just wraps around type X */
+#[repr(u64)]
+pub enum Enum20<X> {
+  Enum20_0(X),
+  Enum20_1(X),
+  Enum20_2(X),
+  Enum20_3(X),
+  Enum20_4(X),
+  Enum20_5(X),
+  Enum20_6(X),
+  Enum20_7(X),
+  Enum20_8(X),
+  Enum20_9(X),
+  Enum20_10(X),
+  Enum20_11(X),
+  Enum20_12(X),
+  Enum20_13(X),
+  Enum20_14(X),
+  Enum20_15(X),
+  Enum20_16(X),
+  Enum20_17(X),
+  Enum20_18(X),
+  Enum20_19(X),
+}
+
+pub fn enum20_list_proj<'a> (x:&'a Enum20<List<u64>>) -> &'a List<u64> {
+  match x {
+      Enum20::Enum20_0(l) => l,
+      Enum20::Enum20_1(l) => l,
+      Enum20::Enum20_2(l) => l,
+      Enum20::Enum20_3(l) => l,
+      Enum20::Enum20_4(l) => l,
+      Enum20::Enum20_5(l) => l,
+      Enum20::Enum20_6(l) => l,
+      Enum20::Enum20_7(l) => l,
+      Enum20::Enum20_8(l) => l,
+      Enum20::Enum20_9(l) => l,
+      Enum20::Enum20_10(l) => l,
+      Enum20::Enum20_11(l) => l,
+      Enum20::Enum20_12(l) => l,
+      Enum20::Enum20_13(l) => l,
+      Enum20::Enum20_14(l) => l,
+      Enum20::Enum20_15(l) => l,
+      Enum20::Enum20_16(l) => l,
+      Enum20::Enum20_17(l) => l,
+      Enum20::Enum20_18(l) => l,
+      Enum20::Enum20_19(l) => l,
+  }
+}
+
+/* A non-empty list type with 20 separate constructors */
+#[repr(u64)]
+pub enum List10<X> {
+  List10Head(X),
+  List10_0(X,Box<List10<X>>),
+  List10_1(X,Box<List10<X>>),
+  List10_2(X,Box<List10<X>>),
+  List10_3(X,Box<List10<X>>),
+  List10_4(X,Box<List10<X>>),
+  List10_5(X,Box<List10<X>>),
+  List10_6(X,Box<List10<X>>),
+  List10_7(X,Box<List10<X>>),
+  List10_8(X,Box<List10<X>>),
+  List10_9(X,Box<List10<X>>),
+}
+
+pub fn list10_head<'a> (x:&'a List10<List<u64>>) -> &'a List<u64> {
+  match x {
+      List10::List10Head(l) => l,
+      List10::List10_0(l,_) => l,
+      List10::List10_1(l,_) => l,
+      List10::List10_2(l,_) => l,
+      List10::List10_3(l,_) => l,
+      List10::List10_4(l,_) => l,
+      List10::List10_5(l,_) => l,
+      List10::List10_6(l,_) => l,
+      List10::List10_7(l,_) => l,
+      List10::List10_8(l,_) => l,
+      List10::List10_9(l,_) => l,
+  }
+}
+
+
+/* A non-empty list type with 20 separate constructors */
+#[repr(u64)]
+pub enum List20<X> {
+  List20Head(X),
+  List20_0(X,Box<List20<X>>),
+  List20_1(X,Box<List20<X>>),
+  List20_2(X,Box<List20<X>>),
+  List20_3(X,Box<List20<X>>),
+  List20_4(X,Box<List20<X>>),
+  List20_5(X,Box<List20<X>>),
+  List20_6(X,Box<List20<X>>),
+  List20_7(X,Box<List20<X>>),
+  List20_8(X,Box<List20<X>>),
+  List20_9(X,Box<List20<X>>),
+  List20_10(X,Box<List20<X>>),
+  List20_11(X,Box<List20<X>>),
+  List20_12(X,Box<List20<X>>),
+  List20_13(X,Box<List20<X>>),
+  List20_14(X,Box<List20<X>>),
+  List20_15(X,Box<List20<X>>),
+  List20_16(X,Box<List20<X>>),
+  List20_17(X,Box<List20<X>>),
+  List20_18(X,Box<List20<X>>),
+  List20_19(X,Box<List20<X>>),
+}
+
+pub fn list20_head<'a> (x:&'a List20<List<u64>>) -> &'a List<u64> {
+  match x {
+      List20::List20Head(l) => l,
+      List20::List20_0(l,_) => l,
+      List20::List20_1(l,_) => l,
+      List20::List20_2(l,_) => l,
+      List20::List20_3(l,_) => l,
+      List20::List20_4(l,_) => l,
+      List20::List20_5(l,_) => l,
+      List20::List20_6(l,_) => l,
+      List20::List20_7(l,_) => l,
+      List20::List20_8(l,_) => l,
+      List20::List20_9(l,_) => l,
+      List20::List20_10(l,_) => l,
+      List20::List20_11(l,_) => l,
+      List20::List20_12(l,_) => l,
+      List20::List20_13(l,_) => l,
+      List20::List20_14(l,_) => l,
+      List20::List20_15(l,_) => l,
+      List20::List20_16(l,_) => l,
+      List20::List20_17(l,_) => l,
+      List20::List20_18(l,_) => l,
+      List20::List20_19(l,_) => l,
+  }
+}
diff --git a/heapster-saw/examples/rust_data.saw b/heapster-saw/examples/rust_data.saw
index 9776644e93..2bbbeec57c 100644
--- a/heapster-saw/examples/rust_data.saw
+++ b/heapster-saw/examples/rust_data.saw
@@ -61,6 +61,14 @@ heapster_define_opaque_llvmshape env "HashMap" 64 "T:llvmshape 64, U:llvmshape 6
 // where the type being defined is passed to an opaque or recursvie type
 //heapster_define_rust_type env "pub enum Tree<X> { Leaf (X), Node (Vec<Tree<X>>) }";
 
+// Enum20 type
+heapster_define_rust_type env "pub enum Enum20<X> { Enum20_0(X), Enum20_1(X), Enum20_2(X), Enum20_3(X), Enum20_4(X), Enum20_5(X), Enum20_6(X), Enum20_7(X), Enum20_8(X), Enum20_9(X), Enum20_10(X), Enum20_11(X), Enum20_12(X), Enum20_13(X), Enum20_14(X), Enum20_15(X), Enum20_16(X), Enum20_17(X), Enum20_18(X), Enum20_19(X), }";
+
+// List10 type
+heapster_define_rust_type env "pub enum List10<X> { List10_Head(X,Box<List10<X>>), List10_0(X,Box<List10<X>>), List10_1(X,Box<List10<X>>), List10_2(X,Box<List10<X>>), List10_3(X,Box<List10<X>>), List10_4(X,Box<List10<X>>), List10_5(X,Box<List10<X>>), List10_6(X,Box<List10<X>>), List10_7(X,Box<List10<X>>), List10_8(X,Box<List10<X>>), List10_9(X,Box<List10<X>>), }";
+
+// List20 type
+heapster_define_rust_type env "pub enum List20<X> { List20_Head(X,Box<List20<X>>), List20_0(X,Box<List20<X>>), List20_1(X,Box<List20<X>>), List20_2(X,Box<List20<X>>), List20_3(X,Box<List20<X>>), List20_4(X,Box<List20<X>>), List20_5(X,Box<List20<X>>), List20_6(X,Box<List20<X>>), List20_7(X,Box<List20<X>>), List20_8(X,Box<List20<X>>), List20_9(X,Box<List20<X>>), List20_10(X,Box<List20<X>>), List20_11(X,Box<List20<X>>), List20_12(X,Box<List20<X>>), List20_13(X,Box<List20<X>>), List20_14(X,Box<List20<X>>), List20_15(X,Box<List20<X>>), List20_16(X,Box<List20<X>>), List20_17(X,Box<List20<X>>), List20_18(X,Box<List20<X>>), List20_19(X,Box<List20<X>>), }";
 
 
 /***
@@ -158,6 +166,15 @@ str_struct_new <- heapster_find_symbol env "9StrStruct3new";
 // FIXME: this is the correct version, with the String shape
 heapster_typecheck_fun_rename env str_struct_new "str_struct_new" "(len:bv 64).arg0:memblock(W,0,24,emptysh), arg1:array(0,<len,*1,[(R,0,8) |-> int8<>]), arg2:eq(llvmword(len)) -o arg0:memblock(W,0,24,String<>)";
 
+enum20_list_proj_sym <- heapster_find_symbol env "16enum20_list_proj";
+//heapster_typecheck_fun_rename env enum20_list_proj_sym "enum20_list_proj" "<'a> fn (x:&'a Enum20<List<u64>>) -> &'a List<u64>";
+
+list10_head_sym <- heapster_find_symbol env "11list10_head";
+//heapster_typecheck_fun_rename env list10_head_sym "list10_head" "<'a> fn (x:&'a List10<List<u64>>) -> &'a List<u64>";
+
+list20_head_sym <- heapster_find_symbol env "11list20_head";
+heapster_typecheck_fun_rename env list20_head_sym "list20_head" "<'a> fn (x:&'a List20<List<u64>>) -> &'a List<u64>";
+
 
 /***
  *** Export to Coq
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 37325ad95c..5a2e1ffa7c 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -2165,6 +2165,9 @@ simplImplOut (SImpl_NamedArgRead x npn args off memb) =
 simplImplOut (SImpl_ReachabilityTrans x rp args off _ e) =
   distPerms1 x (ValPerm_Named (recPermName rp) (PExprs_Cons args e) off)
 
+-- | Compute the output permissions of a 'SimplImpl' implication in a binding
+mbSimplImplOut :: Mb ctx (SimplImpl ps_in ps_out) -> Mb ctx (DistPerms ps_out)
+mbSimplImplOut = mbMapCl $(mkClosed [| simplImplOut |])
 
 -- | Apply a 'SimplImpl' implication to the permissions on the top of a
 -- permission set stack, checking that they equal the 'simplImplIn' of the
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index 7e0c779ac5..0a0c8da851 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -4864,7 +4864,7 @@ noExprsInTypeCtx (Member_Step ctx) = noExprsInTypeCtx ctx
 -- | Defines a substitution type @s@ that supports substituting into expression
 -- and permission variables in a given monad @m@
 class MonadBind m => SubstVar s m | s -> m where
-  -- extSubst :: s ctx -> ExprVar a -> s (ctx :> a)
+  extSubst :: s ctx -> ExprVar a -> s (ctx :> a)
   substExprVar :: s ctx -> Mb ctx (ExprVar a) -> m (PermExpr a)
 
 substPermVar :: SubstVar s m => s ctx -> Mb ctx (PermVar a) -> m (ValuePerm a)
@@ -4874,8 +4874,17 @@ substPermVar s mb_x =
     PExpr_Var x -> return $ ValPerm_Var x NoPermOffset
     PExpr_ValPerm p -> return p
 
+-- | Extend a substitution with 0 or more variables
+extSubstMulti :: SubstVar s m => s ctx -> RAssign ExprVar ctx' ->
+                 s (ctx :++: ctx')
+extSubstMulti s MNil = s
+extSubstMulti s (xs :>: x) = extSubst (extSubstMulti s xs) x
+
 -- | Generalized notion of substitution, which says that substitution type @s@
 -- supports substituting into type @a@ in monad @m@
+--
+-- FIXME: the 'Mb' argument should really be a 'MatchedMb', to emphasize that we
+-- expect it to be in fresh pair form
 class SubstVar s m => Substable s a m where
   genSubst :: s ctx -> Mb ctx a -> m a
 
@@ -4893,44 +4902,47 @@ instance (NuMatching a, Substable s a m) => Substable s (NonEmpty a) m where
   genSubst s (mbMatch -> [nuMP| x :| xs |]) =
     (:|) <$> genSubst s x <*> genSubst s xs
 
-instance (Substable s a m, Substable s b m) => Substable s (a,b) m where
-  genSubst s ab = (,) <$> genSubst s (fmap fst ab) <*> genSubst s (fmap snd ab)
+instance (NuMatching a, NuMatching b,
+          Substable s a m, Substable s b m) => Substable s (a,b) m where
+  genSubst s [nuP| (a,b) |] = (,) <$> genSubst s a <*> genSubst s b
 
-instance (Substable s a m,
+instance (NuMatching a, NuMatching b, NuMatching c, Substable s a m,
           Substable s b m, Substable s c m) => Substable s (a,b,c) m where
-  genSubst s abc =
-    (,,) <$> genSubst s (fmap (\(a,_,_) -> a) abc)
-    <*> genSubst s (fmap (\(_,b,_) -> b) abc)
-    <*> genSubst s (fmap (\(_,_,c) -> c) abc)
+  genSubst s [nuP| (a,b,c) |] =
+    (,,) <$> genSubst s a <*> genSubst s b <*> genSubst s c
 
-instance (Substable s a m, Substable s b m,
+instance (NuMatching a, NuMatching b, NuMatching c, NuMatching d,
+          Substable s a m, Substable s b m,
           Substable s c m, Substable s d m) => Substable s (a,b,c,d) m where
-  genSubst s abcd =
-    (,,,) <$> genSubst s (fmap (\(a,_,_,_) -> a) abcd)
-          <*> genSubst s (fmap (\(_,b,_,_) -> b) abcd)
-          <*> genSubst s (fmap (\(_,_,c,_) -> c) abcd)
-          <*> genSubst s (fmap (\(_,_,_,d) -> d) abcd)
+  genSubst s [nuP| (a,b,c,d) |] =
+    (,,,) <$> genSubst s a <*> genSubst s b <*> genSubst s c <*> genSubst s d
 
 instance (NuMatching a, Substable s a m) => Substable s (Maybe a) m where
   genSubst s mb_x = case mbMatch mb_x of
     [nuMP| Just a |] -> Just <$> genSubst s a
     [nuMP| Nothing |] -> return Nothing
 
-instance {-# INCOHERENT #-} (Given (RAssign Proxy ctx), Substable s a m, NuMatching a) => Substable s (Mb ctx a) m where
-   genSubst = genSubstMb given
+instance {-# INCOHERENT #-} (Given (RAssign Proxy (ctx :: RList CrucibleType)),
+                             Substable s a m, NuMatching a) =>
+                            Substable s (Mb ctx a) m where
+  genSubst = genSubstMb given
 
-instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Mb RNil a) m where
-   genSubst = genSubstMb RL.typeCtxProxies
+instance {-# INCOHERENT #-}
+  (Substable s a m, NuMatching a) =>
+  Substable s (Mb (RNil :: RList CrucibleType) a) m where
+  genSubst = genSubstMb RL.typeCtxProxies
 
-instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Binding c a) m where
-   genSubst = genSubstMb RL.typeCtxProxies
+instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) =>
+                            Substable s (Binding (c :: CrucibleType) a) m where
+  genSubst = genSubstMb RL.typeCtxProxies
 
 genSubstMb ::
   Substable s a m =>
   NuMatching a =>
-  RAssign Proxy ctx ->
+  RAssign Proxy (ctx :: RList CrucibleType) ->
   s ctx' -> Mb ctx' (Mb ctx a) -> m (Mb ctx a)
-genSubstMb p s mbmb = mbM (fmap (genSubst s) (mbSwap p mbmb))
+genSubstMb p s mbmb =
+  mbM $ nuMulti p $ \ns -> genSubst (extSubstMulti s ns) (mbCombine p mbmb)
 
 instance SubstVar s m => Substable s (Member ctx a) m where
   genSubst _ mb_memb = return $ mbLift mb_memb
@@ -5278,7 +5290,7 @@ noPermsInCruCtx (Member_Step ctx) = noPermsInCruCtx ctx
 -- No case for Member_Base
 
 instance SubstVar PermSubst Identity where
-  -- extSubst (PermSubst elems) x = PermSubst $ elems :>: PExpr_Var x
+  extSubst (PermSubst elems) x = PermSubst $ elems :>: PExpr_Var x
   substExprVar s x =
     case mbNameBoundP x of
       Left memb -> return $ substLookup s memb
@@ -5352,7 +5364,7 @@ varSubstVar s mb_x =
     Right x -> x
 
 instance SubstVar PermVarSubst Identity where
-  -- extSubst (PermVarSubst elems) x = PermVarSubst $ elems :>: x
+  extSubst s x = PermVarSubst_Cons s x
   substExprVar s x =
     case mbNameBoundP x of
       Left memb -> return $ PExpr_Var $ varSubstLookup s memb
@@ -5467,9 +5479,8 @@ psubstAppend (PartialSubst elems1) (PartialSubst elems2) =
   PartialSubst $ RL.append elems1 elems2
 
 instance SubstVar PartialSubst Maybe where
-  {-
   extSubst (PartialSubst elems) x =
-    PartialSubst $ elems :>: PSubstElem (Just $ PExpr_Var x) -}
+    PartialSubst $ elems :>: PSubstElem (Just $ PExpr_Var x)
   substExprVar s x =
     case mbNameBoundP x of
       Left memb -> psubstLookup s memb
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 3391cc9b0b..b3a665988e 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -2092,6 +2092,19 @@ class NuMatchingAny1 f => ImplTranslateF f ext blocks tops ret where
 -- * Translating Permission Implication Constructs
 ----------------------------------------------------------------------
 
+-- | Translate the output permissions of a 'SimplImpl'
+translateSimplImplOut :: Mb ctx (SimplImpl ps_in ps_out) ->
+                         ImpTransM ext blocks tops ret ps ctx
+                         (TypeTrans (PermTransCtx ctx ps_out))
+translateSimplImplOut = translate . mbSimplImplOut
+
+-- | Translate the head output permission of a 'SimplImpl'
+translateSimplImplOutHead :: Mb ctx (SimplImpl ps_in (ps_out :> a)) ->
+                             ImpTransM ext blocks tops ret ps ctx
+                             (TypeTrans (PermTrans ctx a))
+translateSimplImplOutHead =
+  fmap (fmap RL.head) . translate . mbSimplImplOut
+
 -- | Translate a 'SimplImpl' to a function on translation computations
 translateSimplImpl :: Proxy ps -> Mb ctx (SimplImpl ps_in ps_out) ->
                       ImpTransM ext blocks tops ret (ps :++: ps_out) ctx OpenTerm ->
@@ -2177,7 +2190,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     m
 
   [nuMP| SImpl_CastPerm (x::ExprVar a) eqp |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        let prxs_a = MNil :>: (Proxy :: Proxy a)
        let prxs1 = mbLift $ fmap (distPermsToProxies . eqProofPerms) eqp
        let prxs = RL.append prxs_a prxs1
@@ -2473,7 +2486,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          m
 
   [nuMP| SImpl_LLVMArrayToField _ _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: _) -> pctx :>: typeTransF ttrans [])
          m
@@ -2582,7 +2595,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     m
 
   [nuMP| SImpl_SplitLifetime _ f args l _ _ ps_in ps_out |] ->
-    do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
+    do pctx_out_trans <- translateSimplImplOut mb_simpl
        ps_in_tp <- translate1 ps_in
        ps_out_tp <- translate1 ps_out
        x_tp_trans <- translate (mbMap3 ltFuncApply f args l)
@@ -2606,14 +2619,14 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          m
 
   [nuMP| SImpl_SubsumeLifetime _ _ _ _ _ |] ->
-    do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
+    do pctx_out_trans <- translateSimplImplOut mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans_l) ->
            RL.append pctx $ typeTransF pctx_out_trans (transTerms ptrans_l))
          m
 
   [nuMP| SImpl_ContainedLifetimeCurrent _ _ _ _ _ |] ->
-    do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
+    do pctx_out_trans <- translateSimplImplOut mb_simpl
        withPermStackM
          (\(ns :>: l1) -> ns :>: l1 :>: l1)
          (\(pctx :>: ptrans_l) ->
@@ -2624,7 +2637,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          m
 
   [nuMP| SImpl_RemoveContainedLifetime _ _ _ _ _ |] ->
-    do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
+    do pctx_out_trans <- translateSimplImplOut mb_simpl
        withPermStackM
          (\(ns :>: l1 :>: _) -> ns :>: l1)
          (\(pctx :>: ptrans_l :>: _) ->
@@ -2635,7 +2648,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          m
 
   [nuMP| SImpl_WeakenLifetime _ _ _ _ _ |] ->
-    do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
+    do pctx_out_trans <- translateSimplImplOut mb_simpl
        withPermStackM RL.tail
          (\(pctx :>: ptrans_x :>: _) ->
            -- NOTE: lcurrent permissions have no term translations, so we can
@@ -2647,7 +2660,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
   [nuMP| SImpl_MapLifetime l _ ps_in ps_out
                            ps_in' ps_out' ps1 ps2 impl_in impl_out |] ->
     -- First, translate the output permissions and all of the perm lists
-    do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
+    do pctx_out_trans <- translateSimplImplOut mb_simpl
        ps_in_trans <- translate ps_in
        ps_out_trans <- translate ps_out
        ps_in'_trans <- translate ps_in'
@@ -2745,19 +2758,19 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     m
 
   [nuMP| SImpl_DemoteLLVMBlockRW _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) -> pctx :>: typeTransF ttrans (transTerms ptrans))
          m
 
   [nuMP| SImpl_IntroLLVMBlockEmpty x _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM (:>: translateVar x)
          (\pctx -> pctx :>: typeTransF ttrans [unitOpenTerm])
          m
 
   [nuMP| SImpl_CoerceLLVMBlockEmpty _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: _) -> pctx :>: typeTransF ttrans [unitOpenTerm])
          m
@@ -2766,7 +2779,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     do let w = natVal2 mb_bp
        let w_term = natOpenTerm w
        len_term <- translate1 $ fmap llvmBlockLen mb_bp
-       ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+       ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: _) ->
            let arr_term =
@@ -2776,7 +2789,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          m
 
   [nuMP| SImpl_IntroLLVMBlockSeqEmpty _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans [pairOpenTerm (transTerm1 ptrans)
@@ -2784,7 +2797,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          m
 
   [nuMP| SImpl_ElimLLVMBlockSeqEmpty _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans [pairLeftOpenTerm (transTerm1 ptrans)])
@@ -2796,7 +2809,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
   [nuMP| SImpl_IntroLLVMBlockNamed _ bp nmsh |]
     | [nuMP| RecShapeBody _ _ fold_ids |] <- mbMatch $ fmap namedShapeBody nmsh
     , [nuMP| PExpr_NamedShape _ _ _ args |] <- mbMatch $ fmap llvmBlockShape bp ->
-      do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+      do ttrans <- translateSimplImplOutHead mb_simpl
          args_trans <- translate args
          fold_id <-
            case fold_ids of
@@ -2812,7 +2825,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
 
   -- Intro for a defined named shape (the other case) is a no-op
     | [nuMP| DefinedShapeBody _ |] <- mbMatch $ fmap namedShapeBody nmsh ->
-      do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+      do ttrans <- translateSimplImplOutHead mb_simpl
          withPermStackM id
            (\(pctx :>: ptrans) ->
              pctx :>: typeTransF ttrans [transTerm1 ptrans])
@@ -2826,7 +2839,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
   [nuMP| SImpl_ElimLLVMBlockNamed _ bp nmsh |]
     | [nuMP| RecShapeBody _ _ fold_ids |] <- mbMatch $ fmap namedShapeBody nmsh
     , [nuMP| PExpr_NamedShape _ _ _ args |] <- mbMatch $ fmap llvmBlockShape bp ->
-      do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+      do ttrans <- translateSimplImplOutHead mb_simpl
          args_trans <- translate args
          unfold_id <-
            case fold_ids of
@@ -2842,7 +2855,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
 
   -- Intro for a defined named shape (the other case) is a no-op
     | [nuMP| DefinedShapeBody _ |] <- mbMatch $ fmap namedShapeBody nmsh ->
-      do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+      do ttrans <- translateSimplImplOutHead mb_simpl
          withPermStackM id
            (\(pctx :>: ptrans) ->
              pctx :>: typeTransF ttrans [transTerm1 ptrans])
@@ -2851,28 +2864,28 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     | otherwise -> fail "translateSimplImpl: ElimLLVMBlockNamed, unknown named shape"
 
   [nuMP| SImpl_IntroLLVMBlockFromEq _ _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM RL.tail
          (\(pctx :>: _ :>: ptrans) ->
            pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
 
   [nuMP| SImpl_IntroLLVMBlockPtr _ _ _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans (transTerms ptrans))
          m
 
   [nuMP| SImpl_ElimLLVMBlockPtr _ _ _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans (transTerms ptrans))
          m
 
   [nuMP| SImpl_IntroLLVMBlockField _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans [transTupleTerm ptrans])
@@ -2892,21 +2905,21 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          m
 
   [nuMP| SImpl_IntroLLVMBlockArray _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
 
   [nuMP| SImpl_ElimLLVMBlockArray _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
 
   [nuMP| SImpl_IntroLLVMBlockSeq _ _ _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM RL.tail
          (\(pctx :>: ptrans1 :>: ptrans2) ->
            let pair_term =
@@ -2915,7 +2928,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          m
 
   [nuMP| SImpl_ElimLLVMBlockSeq _ _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans [pairLeftOpenTerm (transTerm1 ptrans),
@@ -2923,32 +2936,32 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          m
 
   [nuMP| SImpl_IntroLLVMBlockOr _ _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) -> pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
 
   [nuMP| SImpl_ElimLLVMBlockOr _ _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) -> pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
 
   [nuMP| SImpl_IntroLLVMBlockEx _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) -> pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
 
   [nuMP| SImpl_ElimLLVMBlockEx _ _ |] ->
-    do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) -> pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
 
   [nuMP| SImpl_FoldNamed _ (NamedPerm_Rec rp) args _ |] ->
     do args_trans <- translate args
-       ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+       ttrans <- translateSimplImplOutHead mb_simpl
        let fold_ident = mbLift $ fmap recPermFoldFun rp
        withPermStackM id
          (\(pctx :>: ptrans_x) ->
@@ -2960,7 +2973,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
 
   [nuMP| SImpl_UnfoldNamed _ (NamedPerm_Rec rp) args _ |] ->
     do args_trans <- translate args
-       ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+       ttrans <- translateSimplImplOutHead mb_simpl
        let unfold_ident = mbLift $ fmap recPermUnfoldFun rp
        withPermStackM id
          (\(pctx :>: ptrans_x) ->
@@ -2994,37 +3007,37 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
   -}
 
   [nuMP| SImpl_NamedToConj _ _ _ _ |] ->
-    do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do tp_trans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
 
   [nuMP| SImpl_NamedFromConj _ _ _ _ |] ->
-    do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do tp_trans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
 
   [nuMP| SImpl_NamedArgAlways _ _ _ _ _ _ |] ->
-    do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do tp_trans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
 
   [nuMP| SImpl_NamedArgCurrent _ _ _ _ _ _ |] ->
-    do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do tp_trans <- translateSimplImplOutHead mb_simpl
        withPermStackM RL.tail
          (\(pctx :>: ptrans :>: _) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
 
   [nuMP| SImpl_NamedArgWrite _ _ _ _ _ _ |] ->
-    do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do tp_trans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
 
   [nuMP| SImpl_NamedArgRead _ _ _ _ _ |] ->
-    do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+    do tp_trans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
@@ -3033,7 +3046,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     do args_trans <- translate $ mbMap2 PExprs_Cons args e
        y_trans <- translate y
        e_trans <- translate e
-       ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
+       ttrans <- translateSimplImplOutHead mb_simpl
        let trans_ident = mbLift $ fmap recPermTransMethod rp
        withPermStackM RL.tail
          (\(pctx :>: ptrans_x :>: ptrans_y) ->