diff --git a/src/cddl/pulse/CDDL.Pulse.AST.Parse.fst b/src/cddl/pulse/CDDL.Pulse.AST.Parse.fst
new file mode 100644
index 000000000..40c54e3e8
--- /dev/null
+++ b/src/cddl/pulse/CDDL.Pulse.AST.Parse.fst
@@ -0,0 +1,127 @@
+module CDDL.Pulse.AST.Parse
+include CDDL.Pulse.AST.Base
+include CDDL.Pulse.AST.Parse.ElemType
+include CDDL.Pulse.AST.Types
+open Pulse.Lib.Pervasives
+module Cbor = CBOR.Spec.API.Format
+
+[@@sem_attr]
+type parse_env
+  (#cbor_t: Type)
+  (vmatch: perm -> cbor_t -> Cbor.cbor -> slprop)
+  (#se: sem_env)
+  (#s_env: target_type_env se.se_bound)
+  (r_env: rel_env s_env)
+  (sp_env: spec_env se s_env.te_type)
+= (n: typ_name se.se_bound) -> impl_zero_copy_parse vmatch (sp_env.tp_spec_typ n).parser (r_env n).sem_rel
+
+[@@sem_attr]
+let ancillary_parse_env
+  (#cbor_t: Type)
+  (vmatch: perm -> cbor_t -> Cbor.cbor -> slprop)
+  (#cbor_array_iterator_t: Type0)
+  (cbor_array_iterator_match: perm -> cbor_array_iterator_t -> list Cbor.cbor -> slprop)  
+  (#se: sem_env)
+  (#s_env: target_type_env se.se_bound)
+  (r_env: rel_env s_env)
+  (sp_env: spec_env se s_env.te_type)
+= (t: typ) -> (t_wf: ast0_wf_typ t { spec_wf_typ se true t t_wf }) -> option (impl_zero_copy_parse vmatch (spec_of_wf_typ sp_env t_wf).parser (impl_type_sem vmatch cbor_array_iterator_match r_env (target_type_of_wf_typ t_wf)).sem_rel)
+
+[@@sem_attr]
+let ancillary_parse_env_extend
+  (#cbor_t: Type)
+  (#vmatch: perm -> cbor_t -> Cbor.cbor -> slprop)
+  (#cbor_array_iterator_t: Type0)
+  (#cbor_array_iterator_match: perm -> cbor_array_iterator_t -> list Cbor.cbor -> slprop)  
+  (#se: sem_env)
+  (#s_env: target_type_env se.se_bound)
+  (#r_env: rel_env s_env)
+  (#sp_env: spec_env se s_env.te_type)
+  (env1: ancillary_parse_env vmatch cbor_array_iterator_match r_env sp_env)
+  (#se2: sem_env)
+  (#s_env2: target_type_env se2.se_bound)
+  (r_env2: rel_env s_env2 {
+    rel_env_included r_env r_env2
+  })
+  (sp_env2: spec_env se2 s_env2.te_type {
+    spec_env_included sp_env sp_env2
+  })
+: Tot (ancillary_parse_env vmatch cbor_array_iterator_match r_env2 sp_env2)
+= fun t t_wf ->
+  if bounded_wf_typ se.se_bound t t_wf
+  then begin
+    (env1 t t_wf)
+  end
+  else None
+
+module U64 = FStar.UInt64
+module U8 = FStar.UInt8
+module I64 = FStar.Int64
+module V = CDDL.Pulse.AST.Validate
+module SZ = FStar.SizeT
+
+[@@sem_attr]
+let rec impl_zero_copy_type
+  (#cbor_t #t2 #t_arr #t_map: Type0)
+  (#vmatch: (perm -> cbor_t -> Cbor.cbor -> slprop))
+  (#vmatch2: (perm -> t2 -> (Cbor.cbor & Cbor.cbor) -> slprop))
+  (#cbor_array_iterator_match: (perm -> t_arr -> list Cbor.cbor -> slprop))
+  (#cbor_map_iterator_match: (perm -> t_map -> list (Cbor.cbor & Cbor.cbor) -> slprop))
+  (impl: cbor_impl vmatch vmatch2 cbor_array_iterator_match cbor_map_iterator_match)
+  (#se: sem_env)
+  (v_env: V.validator_env vmatch se)
+  (#s_env: target_type_env se.se_bound)
+  (r_env: rel_env s_env)
+  (sp_env: spec_env se s_env.te_type)
+  (p_env: parse_env vmatch r_env sp_env)
+  (ancillary: ancillary_parse_env vmatch cbor_array_iterator_match r_env sp_env)
+  (#t: typ)
+  (t_wf: ast0_wf_typ t {
+    spec_wf_typ se true t t_wf /\ SZ.fits_u64
+  })
+: Pure (either (impl_zero_copy_parse vmatch (spec_of_wf_typ sp_env t_wf).parser (impl_type_sem vmatch cbor_array_iterator_match r_env (target_type_of_wf_typ t_wf)).sem_rel) (t': typ & ast0_wf_typ t'))
+    (requires True)
+    (ensures (fun res -> match res with
+    | Inl _ -> True
+    | Inr (| t', t_wf' |) -> spec_wf_typ se true t' t_wf'
+    ))
+    (decreases t_wf)
+= match t_wf with
+  | WfTRewrite _ _ s ->
+    impl_zero_copy_type impl v_env r_env sp_env p_env ancillary s
+  | WfTTagged tg _ s ->
+    begin match impl_zero_copy_type impl v_env r_env sp_env p_env ancillary s with
+    | Inr ask -> Inr ask
+    | Inl p ->
+      begin match tg with
+      | None -> Inl (impl_zero_copy_tagged_none impl.cbor_get_tagged_tag impl.cbor_get_tagged_payload p)
+      | Some tag -> Inl (impl_zero_copy_tagged_some impl.cbor_get_tagged_payload (U64.uint_to_t tag) p)
+      end
+    end
+  | WfTChoice _ _ s1 s2 ->
+    begin match impl_zero_copy_type impl v_env r_env sp_env p_env ancillary s1 with
+    | Inr ask -> Inr ask
+    | Inl p1 ->
+      begin match impl_zero_copy_type impl v_env r_env sp_env p_env ancillary s2 with
+      | Inr ask -> Inr ask
+      | Inl p2 -> Inl (impl_zero_copy_choice (V.validate_typ impl v_env true _ s1) p1 p2)
+      end
+    end
+  | WfTElem e -> Inl (impl_zero_copy_elem_type vmatch impl.cbor_get_major_type impl.cbor_destr_int64 impl.cbor_get_string impl.cbor_destr_simple e)
+  | WfTDetCbor _ _ s ->
+    begin match impl_zero_copy_type impl v_env r_env sp_env p_env ancillary s with
+    | Inr ask -> Inr ask
+    | Inl p ->
+      Inl (impl_zero_copy_det_cbor impl.cbor_get_string impl.cbor_det_parse _ p)
+    end
+  | WfTStrSize k _ _ lo hi ->
+    Inl (impl_zero_copy_str_size impl.cbor_get_string (U8.uint_to_t k) (U64.uint_to_t lo) (U64.uint_to_t hi))
+  | WfTIntRange _ _ _ lo hi ->
+    if hi < 0
+    then Inl (impl_copyful_pure_as_zero_copy (impl_copyful_int_range_neg_int64 impl.cbor_destr_int64 (U64.uint_to_t ((-1) - lo)) (U64.uint_to_t ((-1) - hi))))
+    else if lo >= 0
+    then Inl (impl_copyful_pure_as_zero_copy (impl_copyful_int_range_uint64 impl.cbor_destr_int64 (U64.uint_to_t lo) (U64.uint_to_t hi)))
+    else Inl (impl_copyful_pure_as_zero_copy (impl_copyful_int_range_int64 impl.cbor_get_major_type impl.cbor_destr_int64 (I64.int_to_t lo) (I64.int_to_t hi)))
+  | WfTDef n -> Inl (p_env n)
+  | WfTArray _ _ -> admit ()
+  | WfTMap _ _ _ -> admit ()
diff --git a/src/cddl/pulse/CDDL.Pulse.Parse.Base.fst b/src/cddl/pulse/CDDL.Pulse.Parse.Base.fst
index 87ed2a464..644b81d72 100644
--- a/src/cddl/pulse/CDDL.Pulse.Parse.Base.fst
+++ b/src/cddl/pulse/CDDL.Pulse.Parse.Base.fst
@@ -232,6 +232,47 @@ fn impl_zero_copy_ext
 }
 ```
 
+inline_for_extraction noextract [@@noextract_to "krml"]
+```pulse
+fn impl_zero_copy_choice
+    (#ty: Type u#0)
+    (#vmatch: perm -> ty -> cbor -> slprop)
+    (#t1: Ghost.erased typ)
+    (#tgt1: Type0)
+    (#tgt_serializable1: Ghost.erased (tgt1 -> bool))
+    (#ps1: Ghost.erased (parser_spec t1 tgt1 tgt_serializable1))
+    (#impl1: Type0)
+    (#r1: rel impl1 tgt1)
+    (v1: impl_typ vmatch t1)
+    (p1: impl_zero_copy_parse vmatch ps1 r1)
+    (#t2: Ghost.erased typ)
+    (#tgt2: Type0)
+    (#tgt_serializable2: Ghost.erased (tgt2 -> bool))
+    (#ps2: Ghost.erased (parser_spec t2 tgt2 tgt_serializable2))
+    (#impl2: Type0)
+    (#r2: rel impl2 tgt2)
+    (p2: impl_zero_copy_parse vmatch ps2 r2)
+: impl_zero_copy_parse #_ vmatch #(t_choice (Ghost.reveal t1) (Ghost.reveal t2)) #(either tgt1 tgt2) #(spec_choice_serializable (Ghost.reveal tgt_serializable1) (Ghost.reveal tgt_serializable2)) (parser_spec_choice (Ghost.reveal ps1) (Ghost.reveal ps2) (spec_choice_serializable (Ghost.reveal tgt_serializable1) (Ghost.reveal tgt_serializable2))) #(either impl1 impl2) (rel_either r1 r2)
+=
+    (c: ty)
+    (#p: perm)
+    (#v: Ghost.erased cbor)
+{
+  let test = v1 c;
+  if test {
+    let res = p1 c;
+    with v' . assert (r1 res v');
+    fold (rel_either r1 r2 (Inl res) (Inl v'));
+    Inl res
+  } else {
+    let res = p2 c;
+    with v' . assert (r2 res v');
+    fold (rel_either r1 r2 (Inr res) (Inr v'));
+    Inr res
+  }
+}
+```
+
 // A parser implementation that skips some data instead of reading
 // it. This parser implementation has no equivalent serializer
 
diff --git a/src/cddl/pulse/CDDL.Pulse.Parse.Misc.fst b/src/cddl/pulse/CDDL.Pulse.Parse.Misc.fst
index 13b4053e6..a7a3a8e7d 100644
--- a/src/cddl/pulse/CDDL.Pulse.Parse.Misc.fst
+++ b/src/cddl/pulse/CDDL.Pulse.Parse.Misc.fst
@@ -446,7 +446,7 @@ fn impl_zero_copy_det_cbor
     (#ty: Type u#0)
     (#vmatch: perm -> ty -> cbor -> slprop)
     (#ty': Type0)
-    (#vmatch': perm -> ty -> cbor -> slprop)
+    (#vmatch': perm -> ty' -> cbor -> slprop)
     (cbor_destr_string: get_string_t vmatch)
     (cbor_det_parse: cbor_det_parse_t vmatch')
     (#t: Ghost.erased typ)
diff --git a/src/cddl/spec/CDDL.Spec.AST.Base.fst b/src/cddl/spec/CDDL.Spec.AST.Base.fst
index 3e3d28017..b0b6d24af 100644
--- a/src/cddl/spec/CDDL.Spec.AST.Base.fst
+++ b/src/cddl/spec/CDDL.Spec.AST.Base.fst
@@ -1111,88 +1111,89 @@ and ast0_wf_validate_map_group
     ast0_wf_validate_map_group left_elems left_tables (GZeroOrMore (GMapElem () false key value)) left_elems (left_tables `Spec.t_choice` v_key)
 *)
 
+[@@sem_env]
 let rec bounded_wf_typ
   (env: name_env)
   (t: typ)
   (wf: ast0_wf_typ t)
-: GTot prop
+: Tot bool
   (decreases wf)
 = match wf with
 | WfTRewrite t t' s' ->
-  typ_bounded env t /\
-  typ_bounded env t' /\
+  typ_bounded env t &&
+  typ_bounded env t' &&
   bounded_wf_typ env _ s'
 | WfTArray g s ->
   bounded_wf_array_group env g s
 | WfTTagged tag t' s' ->
   begin match tag with
-  | None -> True
+  | None -> true
   | Some tag ->
-    0 <= tag /\ tag < pow2 64
-  end /\
+    0 <= tag && tag < pow2 64
+  end &&
   bounded_wf_typ env t' s'
 | WfTMap g1 (* ty1 ty2 s1 *) g2 s2 ->
-    group_bounded env g1 /\
-    bounded_elab_map_group env g2 /\
+    group_bounded env g1 &&
+    bounded_elab_map_group env g2 &&
 //    bounded_wf_validate_map_group env Spec.t_always_false Spec.t_always_false g1 ty1 ty2 s1 /\
     bounded_wf_parse_map_group env _ s2
 | WfTChoice t1 t2 s1 s2 ->
-  typ_bounded env t1 /\
-  typ_bounded env t2 /\
-  bounded_wf_typ env t1 s1 /\
+  typ_bounded env t1 &&
+  typ_bounded env t2 &&
+  bounded_wf_typ env t1 s1 &&
   bounded_wf_typ env t2 s2
 | WfTElem e -> wf_elem_typ e
 | WfTDetCbor base dest wfdest ->
-  typ_bounded env base /\
-  typ_bounded env dest /\
+  typ_bounded env base &&
+  typ_bounded env dest &&
   bounded_wf_typ env _ wfdest
 | WfTStrSize k base range lo hi ->
-  (k == U8.v Cbor.cbor_major_type_byte_string \/ k == U8.v Cbor.cbor_major_type_text_string) /\
-  typ_bounded env base /\
-  typ_bounded env range /\
-  0 <= lo /\ lo <= hi /\ hi < pow2 64
+  (k = U8.v Cbor.cbor_major_type_byte_string || k = U8.v Cbor.cbor_major_type_text_string) &&
+  typ_bounded env base &&
+  typ_bounded env range &&
+  0 <= lo && lo <= hi && hi < pow2 64
 | WfTIntRange base_from base_inclusive base_to from to ->
-  typ_bounded env base_from /\
-  typ_bounded env base_to /\
-  from <= to /\
+  typ_bounded env base_from &&
+  typ_bounded env base_to &&
+  from <= to &&
   begin if from >= 0
   then to < pow2 64
   else if to < 0
   then from >= - pow2 64
-  else (from >= - pow2 63 /\ to < pow2 63)
+  else (from >= - pow2 63 && to < pow2 63)
   end
 | WfTDef n ->
-  env n == Some NType
+  env n = Some NType
 
 and bounded_wf_array_group
   (env: name_env)
   (g: group)
   (wf: ast0_wf_array_group g)
-: GTot prop
+: Tot bool
   (decreases wf)
 = match wf with
 | WfAElem _ key ty prf ->
-  typ_bounded env key /\
+  typ_bounded env key &&
   bounded_wf_typ env ty prf
 | WfAZeroOrOne g s ->
-  group_bounded env g /\
+  group_bounded env g &&
   bounded_wf_array_group env g s
 | WfAZeroOrOneOrMore g s g' ->
-  group_bounded env g /\
+  group_bounded env g &&
   bounded_wf_array_group env g s
 | WfAConcat g1 g2 s1 s2 ->
-  group_bounded env g1 /\
-  group_bounded env g2 /\
-  bounded_wf_array_group env g1 s1 /\
+  group_bounded env g1 &&
+  group_bounded env g2 &&
+  bounded_wf_array_group env g1 s1 &&
   bounded_wf_array_group env g2 s2
 | WfAChoice g1 g2 s1 s2 ->
-  group_bounded env g1 /\
-  group_bounded env g2 /\
-  bounded_wf_array_group env g1 s1 /\
+  group_bounded env g1 &&
+  group_bounded env g2 &&
+  bounded_wf_array_group env g1 s1 &&
   bounded_wf_array_group env g2 s2
 | WfARewrite g1 g2 s2 ->
-  group_bounded env g1 /\
-  group_bounded env g2 /\
+  group_bounded env g1 &&
+  group_bounded env g2 &&
   bounded_wf_array_group env g2 s2
 (*  
 | WfADef n ->
@@ -1203,28 +1204,28 @@ and bounded_wf_parse_map_group
   (env: name_env)
   (g: elab_map_group)
   (wf: ast0_wf_parse_map_group g)
-: GTot prop
+: Tot bool
   (decreases wf)
 = match wf with
 | WfMChoice g1' s1 g2' s2 ->
-    bounded_elab_map_group env g1' /\
-    bounded_wf_parse_map_group env g1' s1 /\
-    bounded_elab_map_group env g2' /\
+    bounded_elab_map_group env g1' &&
+    bounded_wf_parse_map_group env g1' s1 &&
+    bounded_elab_map_group env g2' &&
     bounded_wf_parse_map_group env g2' s2
 | WfMConcat g1 s1 g2 s2 ->
-    bounded_elab_map_group env g1 /\
-    bounded_wf_parse_map_group env g1 s1 /\
-    bounded_elab_map_group env g2 /\
+    bounded_elab_map_group env g1 &&
+    bounded_wf_parse_map_group env g1 s1 &&
+    bounded_elab_map_group env g2 &&
     bounded_wf_parse_map_group env g2 s2
 | WfMZeroOrOne g s ->
-    bounded_elab_map_group env g /\
+    bounded_elab_map_group env g &&
     bounded_wf_parse_map_group env g s
 | WfMLiteral cut key value s ->
-    wf_literal key /\
+    wf_literal key &&
     bounded_wf_typ env value s
 | WfMZeroOrMore key key_except value s_key s_key_except s_value ->
-    bounded_wf_typ env key s_key /\
-    bounded_wf_typ env key_except s_key_except /\
+    bounded_wf_typ env key s_key &&
+    bounded_wf_typ env key_except s_key_except &&
     bounded_wf_typ env value s_value
 // TODO: recover named map groups
 
@@ -1661,9 +1662,10 @@ let rec spec_wf_typ_incr
   (wf: ast0_wf_typ g)
 : Lemma
   (requires sem_env_included env env' /\
-    spec_wf_typ env guard_choices g wf
+    bounded_wf_typ env.se_bound g wf
   )
   (ensures
+    spec_wf_typ env guard_choices g wf <==>
       spec_wf_typ env' guard_choices g wf
   )
   (decreases wf)
@@ -1696,9 +1698,10 @@ and spec_wf_array_group_incr
   (wf: ast0_wf_array_group g)
 : Lemma
   (requires sem_env_included env env' /\
-    spec_wf_array_group env g wf
+    bounded_wf_array_group env.se_bound g wf
   )
   (ensures
+    spec_wf_array_group env g wf <==>
       spec_wf_array_group env' g wf
   )
   (decreases wf)
@@ -1767,9 +1770,10 @@ and spec_wf_parse_map_group_incr
   (wf: ast0_wf_parse_map_group g)
 : Lemma
   (requires sem_env_included env env' /\
-    spec_wf_parse_map_group env g wf
+    bounded_wf_parse_map_group env.se_bound g wf
   )
   (ensures
+    spec_wf_parse_map_group env g wf <==>
       spec_wf_parse_map_group env' g wf
   )
   (decreases wf)
@@ -2836,6 +2840,18 @@ let empty_spec_env (e: target_spec_env empty_name_env) : spec_env empty_sem_env
 //  tp_spec_array_group = (fun _ -> false_elim ());
 }
 
+let spec_env_included
+  (#tp_sem1: sem_env)
+  (#tp_tgt1: target_spec_env (tp_sem1.se_bound))
+  (se1: spec_env tp_sem1 tp_tgt1)
+  (#tp_sem2: sem_env)
+  (#tp_tgt2: target_spec_env (tp_sem2.se_bound))
+  (se2: spec_env tp_sem2 tp_tgt2)
+: Tot prop
+= sem_env_included tp_sem1 tp_sem2 /\
+  target_spec_env_included tp_tgt1 tp_tgt2 /\
+  (forall (n: typ_name tp_sem1.se_bound) . se1.tp_spec_typ n == se2.tp_spec_typ n)
+
 let seq_is_bounded64 (s: Seq.seq U8.t) : Tot bool = Seq.length s < pow2 64
 
 let spec_of_elem_typ
@@ -3036,7 +3052,102 @@ and spec_of_wf_map_group
       (typ_sem tp_sem key_except)
       (spec_of_wf_typ env s_value)
 
-#pop-options
+let rec spec_of_wf_typ_incr
+  (#tp_sem: sem_env)
+  (#tp_tgt: target_spec_env (tp_sem.se_bound))
+  (env: spec_env tp_sem tp_tgt)
+  (#tp_sem': sem_env)
+  (#tp_tgt': target_spec_env tp_sem'.se_bound)
+  (env': spec_env tp_sem' tp_tgt')
+  (#t: typ)
+  (wf: ast0_wf_typ t)
+: Lemma
+  (requires (
+    spec_env_included env env' /\
+    spec_wf_typ tp_sem true t wf
+  ))
+  (ensures (
+    spec_of_wf_typ env wf == spec_of_wf_typ env' wf
+  ))
+  (decreases wf)
+  [SMTPatOr [
+    [SMTPat (spec_env_included env env'); SMTPat (spec_of_wf_typ env wf)];
+    [SMTPat (spec_env_included env env'); SMTPat (spec_of_wf_typ env' wf)];
+  ]]
+= match wf with
+  | WfTDetCbor _ _ s
+  | WfTTagged _ _ s
+  | WfTRewrite _ _ s ->
+    spec_of_wf_typ_incr env env' s
+  | WfTArray _ s ->
+    spec_of_wf_array_group_incr env env' s
+  | WfTMap _ _ s2 ->
+    spec_of_wf_map_group_incr env env' s2
+  | WfTChoice _ _ s1 s2 ->
+    spec_of_wf_typ_incr env env' s1;
+    spec_of_wf_typ_incr env env' s2
+  | _ -> ()
+
+and spec_of_wf_array_group_incr
+  (#tp_sem: sem_env)
+  (#tp_tgt: target_spec_env (tp_sem.se_bound))
+  (env: spec_env tp_sem tp_tgt)
+  (#tp_sem': sem_env)
+  (#tp_tgt': target_spec_env tp_sem'.se_bound)
+  (env': spec_env tp_sem' tp_tgt')
+  (#t: group)
+  (wf: ast0_wf_array_group t)
+: Lemma
+  (requires (
+    spec_env_included env env' /\
+    spec_wf_array_group tp_sem t wf
+  ))
+  (ensures (
+    spec_of_wf_array_group env wf == spec_of_wf_array_group env' wf
+  ))
+  (decreases wf)
+= match wf with
+  | WfAElem _ _ _ s ->
+    spec_of_wf_typ_incr env env' s
+  | WfARewrite _ _ s
+  | WfAZeroOrOneOrMore _ s _
+  | WfAZeroOrOne _ s ->
+    spec_of_wf_array_group_incr env env' s
+  | WfAConcat _ _ s1 s2
+  | WfAChoice _ _ s1 s2 ->
+    spec_of_wf_array_group_incr env env' s1;
+    spec_of_wf_array_group_incr env env' s2    
+
+and spec_of_wf_map_group_incr
+  (#tp_sem: sem_env)
+  (#tp_tgt: target_spec_env (tp_sem.se_bound))
+  (env: spec_env tp_sem tp_tgt)
+  (#tp_sem': sem_env)
+  (#tp_tgt': target_spec_env tp_sem'.se_bound)
+  (env': spec_env tp_sem' tp_tgt')
+  (#t: elab_map_group)
+  (wf: ast0_wf_parse_map_group t)
+: Lemma
+  (requires (
+    spec_env_included env env' /\
+    spec_wf_parse_map_group tp_sem t wf
+  ))
+  (ensures (
+    spec_of_wf_map_group env wf == spec_of_wf_map_group env' wf
+  ))
+  (decreases wf)
+= match wf with
+  | WfMChoice _ s1 _ s2
+  | WfMConcat _ s1 _ s2 ->
+    spec_of_wf_map_group_incr env env' s1;
+    spec_of_wf_map_group_incr env env' s2
+  | WfMLiteral _ _ _ s ->
+    spec_of_wf_typ_incr env env' s
+  | WfMZeroOrOne _ s ->
+    spec_of_wf_map_group_incr env env' s
+  | WfMZeroOrMore _ _ _ s1 _ s2 ->
+    spec_of_wf_typ_incr env env' s1;
+    spec_of_wf_typ_incr env env' s2
 
 #restart-solver
 let spec_env_extend_typ
@@ -3050,7 +3161,11 @@ let spec_env_extend_typ
   (senv: spec_env e.e_sem_env wft)
   (t': Ghost.erased Type0)
   (bij: Ghost.erased (Spec.bijection (target_type_sem wft (target_type_of_wf_typ t_wf)) t'))
-: Tot (spec_env (wf_ast_env_extend_typ_with_weak e new_name t t_wf).e_sem_env (target_spec_env_extend e.e_sem_env.se_bound wft new_name NType t'))
+: Pure (spec_env (wf_ast_env_extend_typ_with_weak e new_name t t_wf).e_sem_env (target_spec_env_extend e.e_sem_env.se_bound wft new_name NType t'))
+    (requires True)
+    (ensures fun senv' ->
+      spec_env_included senv senv'
+    )
 = let e' = (wf_ast_env_extend_typ_with_weak e new_name t t_wf) in
   assert (e'.e_sem_env.se_bound == extend_name_env e.e_sem_env.se_bound new_name NType);
   let wft' : target_spec_env e'.e_sem_env.se_bound = coerce_eq () (target_spec_env_extend e.e_sem_env.se_bound wft new_name NType t') in
@@ -3060,3 +3175,5 @@ let spec_env_extend_typ
   }
   in
   senv'
+
+#pop-options
diff --git a/src/cddl/spec/CDDL.Spec.Base.fst b/src/cddl/spec/CDDL.Spec.Base.fst
index 0e50d0a62..de9fa45a6 100644
--- a/src/cddl/spec/CDDL.Spec.Base.fst
+++ b/src/cddl/spec/CDDL.Spec.Base.fst
@@ -158,6 +158,17 @@ let spec_literal (x: Cbor.cbor) : Tot  (spec (t_literal x) unit true) = {
   parser_inj = ();
 }
 
+let spec_choice_serializable
+  (#target1: Type0)
+  (target1_ser: target1 -> bool)
+  (#target2: Type0)
+  (target2_ser: target2 -> bool)
+  (x: target1 `either` target2)
+: Tot bool
+= match x with
+    | Inl x1 -> target1_ser x1
+    | Inr x2 -> target2_ser x2
+
 let parser_spec_choice
   (#source1: typ)
   (#target1: Type0)
@@ -201,21 +212,6 @@ let serializer_spec_choice
   | Inl y -> s1 y
   | Inr y -> s2 y
 
-let spec_choice_serializable
-  (#source1: typ)
-  (#target1: Type0)
-  (#inj1: bool)
-  (p1: spec source1 target1 inj1)
-  (#source2: typ)
-  (#target2: Type0)
-  (#inj2: bool)
-  (p2: spec source2 target2 inj2)
-  (x: target1 `either` target2)
-: Tot bool
-= match x with
-    | Inl x1 -> p1.serializable x1
-    | Inr x2 -> p2.serializable x2
-
 let spec_choice
   (#source1: typ)
   (#target1: Type0)
@@ -227,7 +223,7 @@ let spec_choice
   (p2: spec source2 target2 inj2 { source1 `typ_disjoint` source2 })
 : Tot (spec (source1 `t_choice` source2) (target1 `either` target2) (inj1 && inj2))
 = {
-  serializable = spec_choice_serializable p1 p2;
+  serializable = spec_choice_serializable p1.serializable p2.serializable;
   parser = parser_spec_choice p1.parser p2.parser _;
   serializer = serializer_spec_choice p1.serializer p2.serializer _;
   parser_inj = ();