diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 697872ed4..926b6b6c5 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -82,6 +82,7 @@ jobs:
           CHARON: ${{needs.select-dep-versions.outputs.charon}}
           AENEAS: ${{needs.select-dep-versions.outputs.aeneas}}
         run: |
+          echo 'Using the aeneas commit selected by `select-dep-versions`'
           nix flake update --refresh \
               charon aeneas \
               --override-input charon github:aeneasverif/charon/$CHARON \
@@ -99,6 +100,7 @@ jobs:
           CHARON: ${{needs.select-dep-versions.outputs.charon}}
           EURYDICE: ${{needs.select-dep-versions.outputs.eurydice}}
         run: |
+          echo 'Using the eurydice commit selected by `select-dep-versions`'
           nix flake update --refresh \
               charon eurydice \
               --override-input charon github:aeneasverif/charon/$CHARON \
@@ -117,6 +119,7 @@ jobs:
           EURYDICE: ${{needs.select-dep-versions.outputs.eurydice}}
           LIBCRUX: ${{needs.select-dep-versions.outputs.libcrux}}
         run: |
+          echo 'Using the eurydice and libcrux commits selected by `select-dep-versions`'
           nix flake update --refresh \
               charon eurydice \
               --override-input charon github:aeneasverif/charon/$CHARON \
diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml
index c221df848..4693d42d7 100644
--- a/charon-ml/src/CharonVersion.ml
+++ b/charon-ml/src/CharonVersion.ml
@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.115"
+let supported_charon_version = "0.1.116"
diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml
index 367c12cc4..5d88e3b32 100644
--- a/charon-ml/src/NameMatcher.ml
+++ b/charon-ml/src/NameMatcher.ml
@@ -996,12 +996,15 @@ and ty_to_pattern_aux (ctx : 'fun_body ctx) (c : to_pat_config)
         else Some (ty_to_pattern_aux ctx c m output)
       in
       EArrow (inputs, output)
+  | TError _ -> EVar None
   | TRawPtr (ty, RMut) -> ERawPtr (Mut, ty_to_pattern_aux ctx c m ty)
   | TRawPtr (ty, RShared) -> ERawPtr (Not, ty_to_pattern_aux ctx c m ty)
-  | TFnDef _ -> raise (Failure "Unimplemented: FnDef")
-  | TDynTrait _ -> raise (Failure "Unimplemented: DynTrait")
-  | TNever -> raise (Failure "Unimplemented: Never")
-  | TError _ -> EVar None
+  | _ ->
+      let fmt_env = ctx_to_fmt_env ctx in
+      raise
+        (Failure
+           ("Can't convert type to pattern: "
+           ^ PrintTypes.ty_to_string fmt_env ty))
 
 and trait_ref_item_with_generics_to_pattern (ctx : 'fun_body ctx)
     (c : to_pat_config) (m : constraints) (trait_ref : T.trait_ref)
diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml
index db2934d6d..148693e10 100644
--- a/charon-ml/src/generated/Generated_GAstOfJson.ml
+++ b/charon-ml/src/generated/Generated_GAstOfJson.ml
@@ -197,6 +197,7 @@ and binder_kind_of_json (ctx : of_json_ctx) (js : json) :
         let* x_1 = trait_item_name_of_json ctx x_1 in
         Ok (BKTraitMethod (x_0, x_1))
     | `String "InherentImplBlock" -> Ok BKInherentImplBlock
+    | `String "Dyn" -> Ok BKDyn
     | `String "Other" -> Ok BKOther
     | _ -> Error "")
 
@@ -600,11 +601,13 @@ and discriminant_layout_of_json (ctx : of_json_ctx) (js : json) :
         Ok ({ offset; tag_ty; encoding } : discriminant_layout)
     | _ -> Error "")
 
-and existential_predicate_of_json (ctx : of_json_ctx) (js : json) :
-    (existential_predicate, string) result =
+and dyn_predicate_of_json (ctx : of_json_ctx) (js : json) :
+    (dyn_predicate, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
-    | `Null -> Ok ()
+    | `Assoc [ ("binder", binder) ] ->
+        let* binder = binder_of_json ty_of_json ctx binder in
+        Ok ({ binder } : dyn_predicate)
     | _ -> Error "")
 
 and field_of_json (ctx : of_json_ctx) (js : json) : (field, string) result =
@@ -1790,7 +1793,7 @@ and ty_of_json (ctx : of_json_ctx) (js : json) : (ty, string) result =
         let* x_1 = trait_item_name_of_json ctx x_1 in
         Ok (TTraitType (x_0, x_1))
     | `Assoc [ ("DynTrait", dyn_trait) ] ->
-        let* dyn_trait = existential_predicate_of_json ctx dyn_trait in
+        let* dyn_trait = dyn_predicate_of_json ctx dyn_trait in
         Ok (TDynTrait dyn_trait)
     | `Assoc [ ("FnPtr", fn_ptr) ] ->
         let* fn_ptr =
diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml
index b4c285ac6..5dab6011f 100644
--- a/charon-ml/src/generated/Generated_Types.ml
+++ b/charon-ml/src/generated/Generated_Types.ml
@@ -190,9 +190,43 @@ class virtual ['self] map_ty_base_base =
         { index; name }
   end
 
+(* Ancestors for the ty visitors *)
+class ['self] iter_ty_base =
+  object (self : 'self)
+    inherit [_] iter_ty_base_base
+    method visit_span : 'env -> span -> unit = fun _ _ -> ()
+  end
+
+class ['self] map_ty_base =
+  object (self : 'self)
+    inherit [_] map_ty_base_base
+    method visit_span : 'env -> span -> span = fun _ x -> x
+  end
+
+(** A value of type [T] bound by generic parameters. Used in any context where
+    we're adding generic parameters that aren't on the top-level item, e.g.
+    [for<'a>] clauses (uses [RegionBinder] for now), trait methods, GATs (TODO).
+*)
+type 'a0 binder = {
+  binder_params : generic_params;
+  binder_value : 'a0;
+      (** Named this way to highlight accesses to the inner value that might be
+          handling parameters incorrectly. Prefer using helper methods. *)
+}
+
+and binder_kind =
+  | BKTraitMethod of trait_decl_id * trait_item_name
+      (** The parameters of a trait method. Used in the [methods] lists in trait
+          decls and trait impls. *)
+  | BKInherentImplBlock
+      (** The parameters bound in a non-trait [impl] block. Used in the [Name]s
+          of inherent methods. *)
+  | BKDyn  (** Binder used for [dyn Trait] existential predicates. *)
+  | BKOther  (** Some other use of a binder outside the main Charon ast. *)
+
 (** An built-in function identifier, identifying a function coming from a
     standard library. *)
-type builtin_fun_id =
+and builtin_fun_id =
   | BoxNew  (** [alloc::boxed::Box::new] *)
   | ArrayToSliceShared
       (** Cast an array as a slice.
@@ -249,10 +283,26 @@ and builtin_ty =
   | TSlice  (** Primitive type *)
   | TStr  (** Primitive type *)
 
-(** A predicate of the form [exists<T> where T: Trait].
+(** A const generic variable in a signature or binder. *)
+and const_generic_var = {
+  index : const_generic_var_id;
+      (** Index identifying the variable among other variables bound at the same
+          level. *)
+  name : string;  (** Const generic name *)
+  ty : literal_type;  (** Type of the const generic *)
+}
 
-    TODO: store something useful here *)
-and existential_predicate = unit
+(** The contents of a [dyn Trait] type. *)
+and dyn_predicate = {
+  binder : ty binder;
+      (** This binder binds a single type [T], which is considered existentially
+          quantified. The predicates in the binder apply to [T] and represent
+          the [dyn Trait] constraints. E.g. [dyn Iterator<Item=u32> + Send] is
+          represented as [exists<T: Iterator<Item=u32> + Send> T].
+
+          Only the first trait clause may have methods. We use the vtable of
+          this trait in the [dyn Trait] pointer metadata. *)
+}
 
 and fn_ptr = { func : fun_id_or_trait_method_ref; generics : generic_args }
 
@@ -286,9 +336,31 @@ and generic_args = {
   trait_refs : trait_ref list;
 }
 
+(** Generic parameters for a declaration. We group the generics which come from
+    the Rust compiler substitutions (the regions, types and const generics) as
+    well as the trait clauses. The reason is that we consider that those are
+    parameters that need to be filled. We group in a different place the
+    predicates which are not trait clauses, because those enforce constraints
+    but do not need to be filled with witnesses/instances. *)
+and generic_params = {
+  regions : region_var list;
+  types : type_var list;
+  const_generics : const_generic_var list;
+  trait_clauses : trait_clause list;
+  regions_outlive : (region, region) outlives_pred region_binder list;
+      (** The first region in the pair outlives the second region *)
+  types_outlive : (ty, region) outlives_pred region_binder list;
+      (** The type outlives the region *)
+  trait_type_constraints : trait_type_constraint region_binder list;
+      (** Constraints over trait associated types *)
+}
+
 (** Reference to a global declaration. *)
 and global_decl_ref = { id : global_decl_id; generics : generic_args }
 
+(** .0 outlives .1 *)
+and ('a0, 'a1) outlives_pred = 'a0 * 'a1
+
 and ref_kind = RMut | RShared
 
 and region =
@@ -312,6 +384,17 @@ and region_id = (RegionId.id[@visitors.opaque])
 (** A region variable in a signature or binder. *)
 and region_var = (region_id, string option) indexed_var
 
+(** A trait predicate in a signature, of the form [Type: Trait<Args>]. This
+    functions like a variable binder, to which variables of the form
+    [TraitRefKind::Clause] can refer to. *)
+and trait_clause = {
+  clause_id : trait_clause_id;
+      (** Index identifying the clause among other clauses bound at the same
+          level. *)
+  span : span option;
+  trait : trait_decl_ref region_binder;  (** The trait that is implemented. *)
+}
+
 (** A predicate of the form [Type: Trait<Args>].
 
     About the generics, if we write:
@@ -404,6 +487,19 @@ and trait_instance_id =
       (** The automatically-generated implementation for [dyn Trait]. *)
   | UnknownTrait of string  (** For error reporting. *)
 
+(** A constraint over a trait associated type.
+
+    Example:
+    {@rust[
+      T : Foo<S = String>
+              ^^^^^^^^^^
+    ]} *)
+and trait_type_constraint = {
+  trait_ref : trait_ref;
+  type_name : trait_item_name;
+  ty : ty;
+}
+
 and ty =
   | TAdt of type_decl_ref
       (** An ADT. Note that here ADTs are very general. They can be:
@@ -445,14 +541,7 @@ and ty =
               type Bar; // type associated to the trait Foo
             }
           ]} *)
-  | TDynTrait of existential_predicate
-      (** [dyn Trait]
-
-          This carries an existentially quantified list of predicates, e.g.
-          [exists<T> where T: Into<u64>]. The predicate must quantify over a
-          single type and no any regions or constants.
-
-          TODO: we don't translate this properly yet. *)
+  | TDynTrait of dyn_predicate  (** [dyn Trait] *)
   | TFnPtr of (ty list * ty) region_binder
       (** Function pointer type. This is a literal pointer to a region of memory
           that contains a callable function. This is a function signature with
@@ -491,6 +580,9 @@ and type_id =
           Vec, Cell... The Array and Slice types were initially modelled as
           primitive in the [Ty] type. We decided to move them to built-in types
           as it allows for more uniform treatment throughout the codebase. *)
+
+(** A type variable in a signature or binder. *)
+and type_var = (type_var_id, string) indexed_var
 [@@deriving
   show,
   eq,
@@ -500,7 +592,7 @@ and type_id =
       name = "iter_ty";
       monomorphic = [ "env" ];
       variety = "iter";
-      ancestors = [ "iter_ty_base_base" ];
+      ancestors = [ "iter_ty_base" ];
       nude = true (* Don't inherit VisitorsRuntime *);
     },
   visitors
@@ -508,7 +600,7 @@ and type_id =
       name = "map_ty";
       monomorphic = [ "env" ];
       variety = "map";
-      ancestors = [ "map_ty_base_base" ];
+      ancestors = [ "map_ty_base" ];
       nude = true (* Don't inherit VisitorsRuntime *);
     }]
 
@@ -516,14 +608,12 @@ and type_id =
 class ['self] iter_type_decl_base =
   object (self : 'self)
     inherit [_] iter_ty
-    method visit_span : 'env -> span -> unit = fun _ _ -> ()
     method visit_attr_info : 'env -> attr_info -> unit = fun _ _ -> ()
   end
 
 class ['self] map_type_decl_base =
   object (self : 'self)
     inherit [_] map_ty
-    method visit_span : 'env -> span -> span = fun _ x -> x
     method visit_attr_info : 'env -> attr_info -> attr_info = fun _ x -> x
   end
 
@@ -538,26 +628,6 @@ type abort_kind =
       (** Unwind had to stop for Abi reasons or because cleanup code panicked
           again. *)
 
-(** A value of type [T] bound by generic parameters. Used in any context where
-    we're adding generic parameters that aren't on the top-level item, e.g.
-    [for<'a>] clauses (uses [RegionBinder] for now), trait methods, GATs (TODO).
-*)
-and 'a0 binder = {
-  binder_params : generic_params;
-  binder_value : 'a0;
-      (** Named this way to highlight accesses to the inner value that might be
-          handling parameters incorrectly. Prefer using helper methods. *)
-}
-
-and binder_kind =
-  | BKTraitMethod of trait_decl_id * trait_item_name
-      (** The parameters of a trait method. Used in the [methods] lists in trait
-          decls and trait impls. *)
-  | BKInherentImplBlock
-      (** The parameters bound in a non-trait [impl] block. Used in the [Name]s
-          of inherent methods. *)
-  | BKOther  (** Some other use of a binder outside the main Charon ast. *)
-
 (** Additional information for closures. *)
 and closure_info = {
   kind : closure_kind;
@@ -572,16 +642,6 @@ and closure_info = {
 }
 
 and closure_kind = Fn | FnMut | FnOnce
-
-(** A const generic variable in a signature or binder. *)
-and const_generic_var = {
-  index : const_generic_var_id;
-      (** Index identifying the variable among other variables bound at the same
-          level. *)
-  name : string;  (** Const generic name *)
-  ty : literal_type;  (** Type of the const generic *)
-}
-
 and disambiguator = (Disambiguator.id[@visitors.opaque])
 
 (** Layout of the discriminant. Describes the offset of the discriminant field
@@ -601,25 +661,6 @@ and field = {
 
 and field_id = (FieldId.id[@visitors.opaque])
 
-(** Generic parameters for a declaration. We group the generics which come from
-    the Rust compiler substitutions (the regions, types and const generics) as
-    well as the trait clauses. The reason is that we consider that those are
-    parameters that need to be filled. We group in a different place the
-    predicates which are not trait clauses, because those enforce constraints
-    but do not need to be filled with witnesses/instances. *)
-and generic_params = {
-  regions : region_var list;
-  types : type_var list;
-  const_generics : const_generic_var list;
-  trait_clauses : trait_clause list;
-  regions_outlive : (region, region) outlives_pred region_binder list;
-      (** The first region in the pair outlives the second region *)
-  types_outlive : (ty, region) outlives_pred region_binder list;
-      (** The type outlives the region *)
-  trait_type_constraints : trait_type_constraint region_binder list;
-      (** Constraints over trait associated types *)
-}
-
 (** There are two kinds of [impl] blocks:
     {ul
      {- impl blocks linked to a type ("inherent" impl blocks following Rust
@@ -760,9 +801,6 @@ and layout = {
 *)
 and name = (path_elem list[@visitors.opaque])
 
-(** .0 outlives .1 *)
-and ('a0, 'a1) outlives_pred = 'a0 * 'a1
-
 (** See the comments for [Name] *)
 and path_elem =
   | PeIdent of string * disambiguator
@@ -795,30 +833,6 @@ and tag_encoding =
           Fields:
           - [untagged_variant] *)
 
-(** A trait predicate in a signature, of the form [Type: Trait<Args>]. This
-    functions like a variable binder, to which variables of the form
-    [TraitRefKind::Clause] can refer to. *)
-and trait_clause = {
-  clause_id : trait_clause_id;
-      (** Index identifying the clause among other clauses bound at the same
-          level. *)
-  span : span option;
-  trait : trait_decl_ref region_binder;  (** The trait that is implemented. *)
-}
-
-(** A constraint over a trait associated type.
-
-    Example:
-    {@rust[
-      T : Foo<S = String>
-              ^^^^^^^^^^
-    ]} *)
-and trait_type_constraint = {
-  trait_ref : trait_ref;
-  type_name : trait_item_name;
-  ty : ty;
-}
-
 (** A type declaration.
 
     Types can be opaque or transparent.
@@ -869,9 +883,6 @@ and type_decl_kind =
       (** Used if an error happened during the extraction, and we don't panic on
           error. *)
 
-(** A type variable in a signature or binder. *)
-and type_var = (type_var_id, string) indexed_var
-
 (** A placeholder for the vtable of a trait object. To be implemented in the
     future when [dyn Trait] is fully supported. *)
 and v_table = unit
diff --git a/charon/Cargo.lock b/charon/Cargo.lock
index 601376972..cfbc243af 100644
--- a/charon/Cargo.lock
+++ b/charon/Cargo.lock
@@ -200,7 +200,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "charon"
-version = "0.1.115"
+version = "0.1.116"
 dependencies = [
  "annotate-snippets",
  "anstream",
@@ -788,7 +788,7 @@ checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289"
 [[package]]
 name = "hax-adt-into"
 version = "0.3.1"
-source = "git+https://github.com/AeneasVerif/hax?branch=main#d6d523d2ac84ea9f605ee6da429ab29e2ae9f8c4"
+source = "git+https://github.com/AeneasVerif/hax?branch=main#d30960bf206f65f89567937978ad8fa710eb79e8"
 dependencies = [
  "itertools 0.11.0",
  "proc-macro2",
@@ -799,7 +799,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter"
 version = "0.3.1"
-source = "git+https://github.com/AeneasVerif/hax?branch=main#d6d523d2ac84ea9f605ee6da429ab29e2ae9f8c4"
+source = "git+https://github.com/AeneasVerif/hax?branch=main#d30960bf206f65f89567937978ad8fa710eb79e8"
 dependencies = [
  "extension-traits",
  "hax-adt-into",
@@ -816,7 +816,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter-options"
 version = "0.3.1"
-source = "git+https://github.com/AeneasVerif/hax?branch=main#d6d523d2ac84ea9f605ee6da429ab29e2ae9f8c4"
+source = "git+https://github.com/AeneasVerif/hax?branch=main#d30960bf206f65f89567937978ad8fa710eb79e8"
 dependencies = [
  "hax-adt-into",
  "schemars",
diff --git a/charon/Cargo.toml b/charon/Cargo.toml
index 33e2c2d05..fce7e8150 100644
--- a/charon/Cargo.toml
+++ b/charon/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.115"
+version = "0.1.116"
 authors = [
     "Son Ho <hosonmarc@gmail.com>",
     "Guillaume Boisseau <nadrieril+git@gmail.com>",
diff --git a/charon/src/ast/expressions_utils.rs b/charon/src/ast/expressions_utils.rs
index abcf42d69..7f08947f5 100644
--- a/charon/src/ast/expressions_utils.rs
+++ b/charon/src/ast/expressions_utils.rs
@@ -65,8 +65,8 @@ impl Place {
             Adt(tref) if matches!(tref.id, TypeId::Builtin(BuiltinTy::Box)) => {
                 tref.generics.types[0].clone()
             }
-            Adt(..) | TypeVar(_) | Literal(_) | Never | TraitType(..) | DynTrait(_) | FnPtr(..)
-            | FnDef(..) | Error(..) => panic!("internal type error"),
+            Adt(..) | TypeVar(_) | Literal(_) | Never | TraitType(..) | DynTrait(..)
+            | FnPtr(..) | FnDef(..) | Error(..) => panic!("internal type error"),
         };
         Place {
             ty: proj_ty,
@@ -122,7 +122,7 @@ impl ProjectionElem {
                     Adt(tref) if matches!(tref.id, TypeId::Builtin(BuiltinTy::Box)) => {
                         tref.generics.types[0].clone()
                     }
-                    Adt(..) | TypeVar(_) | Literal(_) | Never | TraitType(..) | DynTrait(_)
+                    Adt(..) | TypeVar(_) | Literal(_) | Never | TraitType(..) | DynTrait(..)
                     | FnPtr(..) | FnDef(..) | Error(..) => {
                         // Type error
                         return Err(());
diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs
index 8900c22e3..585acd5bb 100644
--- a/charon/src/ast/types.rs
+++ b/charon/src/ast/types.rs
@@ -229,6 +229,8 @@ pub enum BinderKind {
     TraitMethod(TraitDeclId, TraitItemName),
     /// The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods.
     InherentImplBlock,
+    /// Binder used for `dyn Trait` existential predicates.
+    Dyn,
     /// Some other use of a binder outside the main Charon ast.
     Other,
 }
@@ -272,12 +274,6 @@ pub struct GenericParams {
     pub trait_type_constraints: Vector<TraitTypeConstraintId, RegionBinder<TraitTypeConstraint>>,
 }
 
-/// A predicate of the form `exists<T> where T: Trait`.
-///
-/// TODO: store something useful here
-#[derive(Debug, Default, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
-pub struct ExistentialPredicate;
-
 /// Where a given predicate came from.
 #[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
 pub enum PredicateOrigin {
@@ -320,6 +316,8 @@ pub enum PredicateOrigin {
     // }
     // ```
     TraitItem(TraitItemName),
+    /// Clauses that are part of a `dyn Trait` type.
+    Dyn,
 }
 
 // rustc counts bytes in layouts as u64
@@ -783,12 +781,7 @@ pub enum TyKind {
     /// ```
     TraitType(TraitRef, TraitItemName),
     /// `dyn Trait`
-    ///
-    /// This carries an existentially quantified list of predicates, e.g. `exists<T> where T:
-    /// Into<u64>`. The predicate must quantify over a single type and no any regions or constants.
-    ///
-    /// TODO: we don't translate this properly yet.
-    DynTrait(ExistentialPredicate),
+    DynTrait(DynPredicate),
     /// Function pointer type. This is a literal pointer to a region of memory that
     /// contains a callable function.
     /// This is a function signature with limited generics: it only supports lifetime generics, not
@@ -902,3 +895,15 @@ pub struct FunSig {
     pub inputs: Vec<Ty>,
     pub output: Ty,
 }
+
+/// The contents of a `dyn Trait` type.
+#[derive(Debug, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
+pub struct DynPredicate {
+    /// This binder binds a single type `T`, which is considered existentially quantified. The
+    /// predicates in the binder apply to `T` and represent the `dyn Trait` constraints.
+    /// E.g. `dyn Iterator<Item=u32> + Send` is represented as `exists<T: Iterator<Item=u32> + Send> T`.
+    ///
+    /// Only the first trait clause may have methods. We use the vtable of this trait in the `dyn
+    /// Trait` pointer metadata.
+    pub binder: Binder<Ty>,
+}
diff --git a/charon/src/ast/visitor.rs b/charon/src/ast/visitor.rs
index 41fe0f58d..532626086 100644
--- a/charon/src/ast/visitor.rs
+++ b/charon/src/ast/visitor.rs
@@ -43,7 +43,7 @@ use indexmap::IndexMap;
     drive(
         AbortKind, Assert, BinOp, Body, BorrowKind, BuiltinFunId, BuiltinIndexOp, BuiltinTy, Call,
         CastKind, ClosureInfo, ClosureKind, ConstGenericVar, ConstGenericVarId,
-        Disambiguator, ExistentialPredicate, Field, FieldId, FieldProjKind, FloatTy, FloatValue,
+        Disambiguator, DynPredicate, Field, FieldId, FieldProjKind, FloatTy, FloatValue,
         FnOperand, FunId, FunIdOrTraitMethodRef, FunSig, ImplElem, IntegerTy, Literal, LiteralTy,
         llbc_ast::Block, llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch,
         Locals, Name, NullOp, Opaque, Operand, PathElem, PlaceKind, ProjectionElem, RawConstantExpr,
@@ -73,7 +73,7 @@ use indexmap::IndexMap;
         llbc_statement: llbc_ast::Statement, ullbc_statement: ullbc_ast::Statement,
         AggregateKind, FnPtr, ItemKind, ItemMeta, Span, ConstantExpr,
         FunDeclId, GlobalDeclId, TypeDeclId, TraitDeclId, TraitImplId,
-        FunDecl, GlobalDecl, TypeDecl, TraitDecl, TraitImpl
+        FunDecl, GlobalDecl, TypeDecl, TraitDecl, TraitImpl,
     )
 )]
 pub trait AstVisitable: Any {
diff --git a/charon/src/bin/charon-driver/translate/mod.rs b/charon/src/bin/charon-driver/translate/mod.rs
index 57b4afd84..fd9f32641 100644
--- a/charon/src/bin/charon-driver/translate/mod.rs
+++ b/charon/src/bin/charon-driver/translate/mod.rs
@@ -11,4 +11,5 @@ pub mod translate_generics;
 pub mod translate_items;
 pub mod translate_meta;
 pub mod translate_predicates;
+pub mod translate_trait_objects;
 pub mod translate_types;
diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs
index 133fe870c..fdefbad10 100644
--- a/charon/src/bin/charon-driver/translate/translate_ctx.rs
+++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs
@@ -75,9 +75,6 @@ pub(crate) struct ItemTransCtx<'tcx, 'ctx> {
     pub parent_trait_clauses: Vector<TraitClauseId, TraitClause>,
     /// (For traits only) accumulated trait clauses on associated types.
     pub item_trait_clauses: HashMap<TraitItemName, Vector<TraitClauseId, TraitClause>>,
-    /// (For method declarations only) the clause id corresponding to the explicit `Self` clause.
-    /// If `None` then we're in a trait declaration and should use `TraitRefKind::Self` instead.
-    pub self_clause_id: Option<TraitClauseId>,
 }
 
 /// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
@@ -171,7 +168,6 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
             binding_levels: Default::default(),
             parent_trait_clauses: Default::default(),
             item_trait_clauses: Default::default(),
-            self_clause_id: Default::default(),
         }
     }
 
diff --git a/charon/src/bin/charon-driver/translate/translate_generics.rs b/charon/src/bin/charon-driver/translate/translate_generics.rs
index d140cd8e0..070992931 100644
--- a/charon/src/bin/charon-driver/translate/translate_generics.rs
+++ b/charon/src/bin/charon-driver/translate/translate_generics.rs
@@ -250,12 +250,6 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
         span: Span,
         mut id: usize,
     ) -> Result<ClauseDbVar, Error> {
-        if self.self_clause_id.is_some() {
-            // We added an extra first clause which hax doesn't know about, so we adapt the index
-            // accordingly.
-            // TODO: more robust tracking of clause ids between hax and charon.
-            id += 1;
-        }
         // The clause indices returned by hax count clauses in order, starting from the parentmost.
         // While adding clauses to a binding level we already need to translate types and clauses,
         // so the innermost item binder may not have all the clauses yet. Hence for that binder we
diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs
index 8dc6d99d0..4e84c0ec2 100644
--- a/charon/src/bin/charon-driver/translate/translate_predicates.rs
+++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs
@@ -215,15 +215,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
                 );
                 // If we are refering to a trait clause, we need to find the relevant one.
                 let mut trait_id = match &impl_source.r#impl {
-                    ImplExprAtom::SelfImpl { .. } => match self.self_clause_id {
-                        None => TraitRefKind::SelfId,
-                        // An explicit `Self` clause is bound at the top-level; we use it instead
-                        // of the implicit `TraitRefKind::SelfId` one.
-                        Some(id) => TraitRefKind::Clause(DeBruijnVar::bound(
-                            self.binding_levels.depth(),
-                            id,
-                        )),
-                    },
+                    ImplExprAtom::SelfImpl { .. } => TraitRefKind::SelfId,
                     ImplExprAtom::LocalBound { index, .. } => {
                         let var = self.lookup_clause_var(span, *index)?;
                         TraitRefKind::Clause(var)
diff --git a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs
new file mode 100644
index 000000000..7714c3206
--- /dev/null
+++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs
@@ -0,0 +1,76 @@
+use crate::translate::{translate_generics::BindingLevel, translate_predicates::PredicateLocation};
+
+use super::translate_ctx::*;
+use charon_lib::ast::*;
+use hax_frontend_exporter as hax;
+
+impl ItemTransCtx<'_, '_> {
+    pub fn check_at_most_one_pred_has_methods(
+        &mut self,
+        span: Span,
+        preds: &hax::GenericPredicates,
+    ) -> Result<(), Error> {
+        // Only the first clause is allowed to have methods.
+        for (clause, _) in preds.predicates.iter().skip(1) {
+            if let hax::ClauseKind::Trait(trait_predicate) = clause.kind.hax_skip_binder_ref() {
+                let trait_def_id = &trait_predicate.trait_ref.def_id;
+                let trait_def = self.hax_def(trait_def_id)?;
+                let has_methods = match trait_def.kind() {
+                    hax::FullDefKind::Trait { items, .. } => items
+                        .iter()
+                        .any(|(assoc, _)| matches!(assoc.kind, hax::AssocKind::Fn { .. })),
+                    hax::FullDefKind::TraitAlias { .. } => false,
+                    _ => unreachable!(),
+                };
+                if has_methods {
+                    raise_error!(
+                        self,
+                        span,
+                        "`dyn Trait` with multiple method-bearing predicates is not supported"
+                    );
+                }
+            }
+        }
+        Ok(())
+    }
+
+    pub fn translate_existential_predicates(
+        &mut self,
+        span: Span,
+        self_ty: &hax::ParamTy,
+        preds: &hax::GenericPredicates,
+        region: &hax::Region,
+    ) -> Result<DynPredicate, Error> {
+        // This is a robustness check: the current version of Rustc
+        // accepts at most one method-bearing predicate in a trait object.
+        // But things may change in the future.
+        self.check_at_most_one_pred_has_methods(span, preds)?;
+
+        // Translate the region outside the binder.
+        let region = self.translate_region(span, region)?;
+        let region = region.move_under_binder();
+
+        // Add a binder that contains the existentially quantified type.
+        self.binding_levels.push(BindingLevel::new(true));
+
+        // Add the existentially quantified type.
+        let ty_id = self
+            .innermost_binder_mut()
+            .push_type_var(self_ty.index, self_ty.name.clone());
+        let ty = TyKind::TypeVar(DeBruijnVar::new_at_zero(ty_id)).into_ty();
+
+        self.innermost_binder_mut()
+            .params
+            .types_outlive
+            .push(RegionBinder::empty(OutlivesPred(ty.clone(), region)));
+        self.register_predicates(preds, PredicateOrigin::Dyn, &PredicateLocation::Base)?;
+
+        let params = self.binding_levels.pop().unwrap().params;
+        let binder = Binder {
+            params: params,
+            skip_binder: ty,
+            kind: BinderKind::Dyn,
+        };
+        Ok(DynPredicate { binder })
+    }
+}
diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs
index 84234d542..983826c24 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -214,10 +214,9 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
                 TyKind::Adt(tref)
             }
 
-            hax::TyKind::Dynamic(_existential_preds, _region, _) => {
-                // TODO: we don't translate the predicates yet because our machinery can't handle
-                // it.
-                TyKind::DynTrait(ExistentialPredicate)
+            hax::TyKind::Dynamic(self_ty, preds, region) => {
+                let pred = self.translate_existential_predicates(span, self_ty, preds, region)?;
+                TyKind::DynTrait(pred)
             }
 
             hax::TyKind::Infer(_) => {
diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs
index a18a56449..855631400 100644
--- a/charon/src/bin/generate-ml/main.rs
+++ b/charon/src/bin/generate-ml/main.rs
@@ -1220,7 +1220,7 @@ fn generate_ml(
                     ancestors: &["ty_base_base"],
                     name: "ty",
                     reduce: false,
-                    extra_types: &[],
+                    extra_types: &["span"],
                 })), &[
                     "TyKind",
                     "TraitImplRef",
@@ -1233,7 +1233,7 @@ fn generate_ml(
                     name: "type_decl",
                     reduce: false,
                     extra_types: &[
-                        "span", "attr_info"
+                        "attr_info"
                     ],
                 })), &[
                     "Binder",
diff --git a/charon/src/options.rs b/charon/src/options.rs
index 6af79f2bc..6dad7eb12 100644
--- a/charon/src/options.rs
+++ b/charon/src/options.rs
@@ -305,6 +305,7 @@ impl CliOpts {
                 Preset::Tests => {
                     self.hide_allocator = !self.raw_boxes;
                     self.rustc_args.push("--edition=2021".to_owned());
+                    self.exclude.push("core::fmt::Formatter".to_owned());
                 }
             }
         }
diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs
index 0149478a5..9fe01e29c 100644
--- a/charon/src/pretty/fmt_with_ctx.rs
+++ b/charon/src/pretty/fmt_with_ctx.rs
@@ -348,9 +348,12 @@ impl<C: AstFormatter> FmtWithCtx<C> for DeclarationGroup {
     }
 }
 
-impl<C: AstFormatter> FmtWithCtx<C> for ExistentialPredicate {
-    fn fmt_with_ctx(&self, _ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "exists(TODO)")
+impl<C: AstFormatter> FmtWithCtx<C> for DynPredicate {
+    fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let ctx = &ctx.push_binder(Cow::Borrowed(&self.binder.params));
+        let ty = self.binder.skip_binder.with_ctx(ctx);
+        let clauses = self.binder.params.formatted_clauses(ctx).format(" + ");
+        write!(f, "exists<{ty}> {clauses}")
     }
 }
 
@@ -1759,7 +1762,9 @@ impl<C: AstFormatter> FmtWithCtx<C> for Ty {
             TyKind::TraitType(trait_ref, name) => {
                 write!(f, "{}::{name}", trait_ref.with_ctx(ctx),)
             }
-            TyKind::DynTrait(pred) => write!(f, "dyn ({})", pred.with_ctx(ctx)),
+            TyKind::DynTrait(pred) => {
+                write!(f, "(dyn {})", pred.with_ctx(ctx))
+            }
             TyKind::FnPtr(io) => {
                 write!(f, "{}", io.with_ctx(ctx))
             }
diff --git a/charon/tests/ui/dyn-trait.out b/charon/tests/ui/dyn-trait.out
index 351a550bc..98e164156 100644
--- a/charon/tests/ui/dyn-trait.out
+++ b/charon/tests/ui/dyn-trait.out
@@ -1,13 +1,20 @@
 # Final LLBC before serialization:
 
-// Full name: core::fmt::Error
-pub struct Error {}
+// Full name: core::cmp::PartialEq
+#[lang_item("eq")]
+pub trait PartialEq<Self, Rhs>
+{
+    fn eq<'_0, '_1> = eq<'_0_0, '_0_1, Self, Rhs>[Self]
+}
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
+// Full name: core::cmp::PartialEq::eq
+#[lang_item("cmp_partialeq_eq")]
+pub fn eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
 where
-    'a : 'a,
+    [@TraitClause0]: PartialEq<Self, Rhs>,
+
+// Full name: core::fmt::Error
+pub struct Error {}
 
 // Full name: core::marker::MetaSized
 #[lang_item("meta_sized")]
@@ -43,6 +50,72 @@ pub fn fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (Formatter<'_2>))
 where
     [@TraitClause0]: Display<Self>,
 
+// Full name: core::marker::Tuple
+#[lang_item("tuple_trait")]
+pub trait Tuple<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+}
+
+// Full name: core::ops::function::FnOnce
+#[lang_item("fn_once")]
+pub trait FnOnce<Self, Args>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: Sized<Args>
+    parent_clause2 : [@TraitClause2]: Tuple<Args>
+    parent_clause3 : [@TraitClause3]: Sized<Self::Output>
+    type Output
+    fn call_once = call_once<Self, Args>[Self]
+}
+
+// Full name: core::ops::function::FnMut
+#[lang_item("fn_mut")]
+pub trait FnMut<Self, Args>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: FnOnce<Self, Args>
+    parent_clause2 : [@TraitClause2]: Sized<Args>
+    parent_clause3 : [@TraitClause3]: Tuple<Args>
+    fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self]
+}
+
+// Full name: core::ops::function::Fn
+#[lang_item("r#fn")]
+pub trait Fn<Self, Args>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: FnMut<Self, Args>
+    parent_clause2 : [@TraitClause2]: Sized<Args>
+    parent_clause3 : [@TraitClause3]: Tuple<Args>
+    fn call<'_0> = call<'_0_0, Self, Args>[Self]
+}
+
+// Full name: core::ops::function::Fn::call
+pub fn call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output
+where
+    [@TraitClause0]: Fn<Self, Args>,
+
+// Full name: core::ops::function::FnMut::call_mut
+pub fn call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output
+where
+    [@TraitClause0]: FnMut<Self, Args>,
+
+// Full name: core::ops::function::FnOnce::call_once
+pub fn call_once<Self, Args>(@1: Self, @2: Args) -> @TraitClause0::Output
+where
+    [@TraitClause0]: FnOnce<Self, Args>,
+
+// Full name: core::option::Option
+#[lang_item("Option")]
+pub enum Option<T>
+where
+    [@TraitClause0]: Sized<T>,
+{
+  None,
+  Some(T),
+}
+
 // Full name: alloc::alloc::Global
 #[lang_item("global_alloc_ty")]
 pub struct Global {}
@@ -81,22 +154,22 @@ where
 }
 
 // Full name: test_crate::construct
-fn construct<T>(@1: T) -> alloc::boxed::Box<dyn (exists(TODO))>[MetaSized<dyn (exists(TODO))>, Sized<Global>]
+fn construct<T>(@1: T) -> alloc::boxed::Box<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : 'static)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized<Global>]
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Display<T>,
     T : 'static,
 
 // Full name: test_crate::destruct
-fn destruct<'_0>(@1: &'_0 (dyn (exists(TODO)))) -> String
+fn destruct<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_0))) -> String
 {
     let @0: String; // return
-    let x@1: &'_ (dyn (exists(TODO))); // arg #1
-    let @2: &'_ (dyn (exists(TODO))); // anonymous local
+    let x@1: &'_ ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)); // arg #1
+    let @2: &'_ ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)); // anonymous local
 
     storage_live(@2)
     @2 := &*(x@1)
-    @0 := {impl ToString for T}::to_string<'_, dyn (exists(TODO))>[MetaSized<dyn (exists(TODO))>, Display<dyn (exists(TODO))>](move (@2))
+    @0 := {impl ToString for T}::to_string<'_, (dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Display<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>](move (@2))
     storage_dead(@2)
     return
 }
@@ -105,13 +178,13 @@ fn destruct<'_0>(@1: &'_0 (dyn (exists(TODO)))) -> String
 fn combine()
 
 // Full name: test_crate::foo
-fn foo<'_0, '_1, T>(@1: &'_0 (dyn (exists(TODO))), @2: &'_1 (dyn (exists(TODO))))
+fn foo<'_0, '_1, T>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a (T))> + _dyn : 'static + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = T)), @2: &'_1 ((dyn exists<_dyn> [@TraitClause0]: PartialEq<_dyn, Option<T>[@TraitClause0]> + _dyn : '_1)))
 where
     [@TraitClause0]: Sized<T>,
 {
     let @0: (); // return
-    let @1: &'_ (dyn (exists(TODO))); // arg #1
-    let @2: &'_ (dyn (exists(TODO))); // arg #2
+    let @1: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a (T))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = T)); // arg #1
+    let @2: &'_ ((dyn exists<_dyn> [@TraitClause0]: PartialEq<_dyn, Option<T>[@TraitClause0]> + _dyn : '_)); // arg #2
 
     @0 := ()
     @0 := ()
@@ -119,10 +192,10 @@ where
 }
 
 // Full name: test_crate::bar
-fn bar<'_0>(@1: &'_0 (dyn (exists(TODO))))
+fn bar<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: for<'_0> Fn<_dyn, (&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_2_0)))> + _dyn : '_0 + for<'_0> @TraitClause1_0::parent_clause1::parent_clause1::Output = ())))
 {
     let @0: (); // return
-    let @1: &'_ (dyn (exists(TODO))); // arg #1
+    let @1: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'_0> Fn<_dyn, (&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_2_0)))> + _dyn : '_ + for<'_0> @TraitClause1_0::parent_clause1::parent_clause1::Output = ())); // arg #1
 
     @0 := ()
     @0 := ()
diff --git a/charon/tests/ui/gosim-demo.out b/charon/tests/ui/gosim-demo.out
index d9a32e509..03081f8cd 100644
--- a/charon/tests/ui/gosim-demo.out
+++ b/charon/tests/ui/gosim-demo.out
@@ -106,12 +106,6 @@ where
 // Full name: core::fmt::Error
 pub struct Error {}
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
-where
-    'a : 'a,
-
 // Full name: core::fmt::Arguments
 #[lang_item("format_arguments")]
 pub opaque type Arguments<'a>
diff --git a/charon/tests/ui/issue-4-slice-try-into-array.out b/charon/tests/ui/issue-4-slice-try-into-array.out
index c33736dc2..bf392ce3b 100644
--- a/charon/tests/ui/issue-4-slice-try-into-array.out
+++ b/charon/tests/ui/issue-4-slice-try-into-array.out
@@ -1,11 +1,5 @@
 # Final LLBC before serialization:
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
-where
-    'a : 'a,
-
 // Full name: core::marker::MetaSized
 #[lang_item("meta_sized")]
 pub trait MetaSized<Self>
diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out
index b94e763eb..b4aaa25ca 100644
--- a/charon/tests/ui/issue-4-traits.out
+++ b/charon/tests/ui/issue-4-traits.out
@@ -1,11 +1,5 @@
 # Final LLBC before serialization:
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
-where
-    'a : 'a,
-
 // Full name: core::marker::MetaSized
 #[lang_item("meta_sized")]
 pub trait MetaSized<Self>
diff --git a/charon/tests/ui/raw-boxes.out b/charon/tests/ui/raw-boxes.out
index bb80ee6b0..dfc01c098 100644
--- a/charon/tests/ui/raw-boxes.out
+++ b/charon/tests/ui/raw-boxes.out
@@ -209,23 +209,6 @@ pub struct NonNull<T> {
   pointer: *const T,
 }
 
-// Full name: core::fmt::FormattingOptions
-pub struct FormattingOptions {
-  flags: u32,
-  width: u16,
-  precision: u16,
-}
-
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub struct Formatter<'a>
-where
-    'a : 'a,
-{
-  options: FormattingOptions,
-  buf: &'a mut (dyn (exists(TODO))),
-}
-
 // Full name: core::result::Result
 #[lang_item("Result")]
 pub enum Result<T, E>
diff --git a/charon/tests/ui/result-unwrap.out b/charon/tests/ui/result-unwrap.out
index 281d73e5a..b0317626a 100644
--- a/charon/tests/ui/result-unwrap.out
+++ b/charon/tests/ui/result-unwrap.out
@@ -30,16 +30,6 @@ fn core::fmt::flags::DEBUG_UPPER_HEX_FLAG() -> u32
 
 const core::fmt::flags::DEBUG_UPPER_HEX_FLAG: u32 = core::fmt::flags::DEBUG_UPPER_HEX_FLAG()
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub struct Formatter<'a>
-where
-    'a : 'a,
-{
-  options: FormattingOptions,
-  buf: &'a mut (dyn (exists(TODO))),
-}
-
 // Full name: core::marker::MetaSized
 #[lang_item("meta_sized")]
 pub trait MetaSized<Self>
@@ -140,7 +130,7 @@ pub fn {impl Debug for u32}::fmt<'_0, '_1, '_2>(@1: &'_0 (u32), @2: &'_1 mut (Fo
     storage_live(@8)
     storage_live(@3)
     storage_live(@4)
-    @4 := copy (((*(f@2)).options).flags)
+    @4 := copy (((*(f@2)).0).flags)
     @7 := core::fmt::flags::DEBUG_LOWER_HEX_FLAG
     @3 := move (@4) & move (@7)
     storage_dead(@4)
@@ -156,7 +146,7 @@ pub fn {impl Debug for u32}::fmt<'_0, '_1, '_2>(@1: &'_0 (u32), @2: &'_1 mut (Fo
     storage_dead(@3)
     storage_live(@5)
     storage_live(@6)
-    @6 := copy (((*(f@2)).options).flags)
+    @6 := copy (((*(f@2)).0).flags)
     @8 := core::fmt::flags::DEBUG_UPPER_HEX_FLAG
     @5 := move (@6) & move (@8)
     storage_dead(@6)
@@ -197,7 +187,7 @@ where
     [@TraitClause0]: Drop<Self>,
 
 // Full name: core::result::unwrap_failed
-fn unwrap_failed<'_0, '_1>(@1: &'_0 (Str), @2: &'_1 (dyn (exists(TODO)))) -> !
+fn unwrap_failed<'_0, '_1>(@1: &'_0 (Str), @2: &'_1 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_1))) -> !
 
 pub fn core::result::{Result<T, E>[@TraitClause0, @TraitClause1]}::unwrap<T, E>(@1: Result<T, E>[@TraitClause0, @TraitClause1]) -> T
 where
@@ -209,7 +199,7 @@ where
     let self@1: Result<T, E>[@TraitClause0, @TraitClause1]; // arg #1
     let e@2: E; // local
     let @3: !; // anonymous local
-    let @4: &'_ (dyn (exists(TODO))); // anonymous local
+    let @4: &'_ ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)); // anonymous local
     let @5: &'_ (E); // anonymous local
 
     storage_live(e@2)
@@ -224,7 +214,7 @@ where
             e@2 := move ((self@1 as variant Result::Err).0)
             storage_live(@4)
             @5 := &e@2
-            @4 := unsize_cast<&'_ (E), &'_ (dyn (exists(TODO))), @TraitClause2>(copy (@5))
+            @4 := unsize_cast<&'_ (E), &'_ ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)), @TraitClause2>(copy (@5))
             @3 := unwrap_failed<'_, '_>(const ("called `Result::unwrap()` on an `Err` value"), move (@4))
         },
     }
diff --git a/charon/tests/ui/simple/dyn-fn.out b/charon/tests/ui/simple/dyn-fn.out
new file mode 100644
index 000000000..dab6b38e6
--- /dev/null
+++ b/charon/tests/ui/simple/dyn-fn.out
@@ -0,0 +1,229 @@
+# Final LLBC before serialization:
+
+// Full name: core::marker::MetaSized
+#[lang_item("meta_sized")]
+pub trait MetaSized<Self>
+
+// Full name: core::marker::Sized
+#[lang_item("sized")]
+pub trait Sized<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+}
+
+// Full name: core::marker::Tuple
+#[lang_item("tuple_trait")]
+pub trait Tuple<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+}
+
+// Full name: core::ops::drop::Drop
+#[lang_item("drop")]
+pub trait Drop<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    fn drop<'_0> = drop<'_0_0, Self>[Self]
+}
+
+// Full name: core::ops::drop::Drop::drop
+pub fn drop<'_0, Self>(@1: &'_0 mut (Self))
+where
+    [@TraitClause0]: Drop<Self>,
+
+// Full name: core::ops::function::FnOnce
+#[lang_item("fn_once")]
+pub trait FnOnce<Self, Args>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: Sized<Args>
+    parent_clause2 : [@TraitClause2]: Tuple<Args>
+    parent_clause3 : [@TraitClause3]: Sized<Self::Output>
+    type Output
+    fn call_once = core::ops::function::FnOnce::call_once<Self, Args>[Self]
+}
+
+// Full name: core::ops::function::FnMut
+#[lang_item("fn_mut")]
+pub trait FnMut<Self, Args>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: FnOnce<Self, Args>
+    parent_clause2 : [@TraitClause2]: Sized<Args>
+    parent_clause3 : [@TraitClause3]: Tuple<Args>
+    fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self]
+}
+
+// Full name: core::ops::function::Fn
+#[lang_item("r#fn")]
+pub trait Fn<Self, Args>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: FnMut<Self, Args>
+    parent_clause2 : [@TraitClause2]: Sized<Args>
+    parent_clause3 : [@TraitClause3]: Tuple<Args>
+    fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self]
+}
+
+pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output
+where
+    [@TraitClause0]: Fn<Self, Args>,
+
+pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output
+where
+    [@TraitClause0]: FnMut<Self, Args>,
+
+pub fn core::ops::function::FnOnce::call_once<Self, Args>(@1: Self, @2: Args) -> @TraitClause0::Output
+where
+    [@TraitClause0]: FnOnce<Self, Args>,
+
+// Full name: test_crate::takes_fn
+fn takes_fn<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_0 + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)))
+{
+    let @0: (); // return
+    let f@1: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)); // arg #1
+    let counter@2: u32; // local
+    let @3: bool; // anonymous local
+    let @4: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)); // anonymous local
+    let @5: (&'_ mut (u32)); // anonymous local
+    let @6: &'_ mut (u32); // anonymous local
+    let @7: &'_ mut (u32); // anonymous local
+
+    storage_live(counter@2)
+    counter@2 := const (0 : u32)
+    storage_live(@3)
+    storage_live(@4)
+    @4 := &*(f@1)
+    storage_live(@5)
+    storage_live(@6)
+    storage_live(@7)
+    @7 := &mut counter@2
+    @6 := &two-phase-mut *(@7)
+    @5 := (move (@6))
+    @3 := Fn<(dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool), (&'_ mut (u32))>::call<'_>(move (@4), move (@5))
+    if move (@3) {
+        storage_dead(@7)
+        storage_dead(@6)
+        storage_dead(@5)
+        storage_dead(@4)
+        @0 := ()
+    }
+    else {
+        storage_dead(@7)
+        storage_dead(@6)
+        storage_dead(@5)
+        storage_dead(@4)
+        @0 := ()
+    }
+    storage_dead(@3)
+    storage_dead(counter@2)
+    @0 := ()
+    return
+}
+
+// Full name: test_crate::gives_fn::closure
+struct closure {}
+
+// Full name: test_crate::gives_fn::{impl Fn<(&'_ mut (u32))> for closure}::call
+fn {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_1>(@1: &'_1 (closure), @2: (&'_0 mut (u32))) -> bool
+{
+    let @0: bool; // return
+    let @1: &'_ (closure); // arg #1
+    let tupled_args@2: (&'_0 mut (u32)); // arg #2
+    let counter@3: &'_ mut (u32); // local
+    let @4: u32; // anonymous local
+
+    storage_live(counter@3)
+    storage_live(@4)
+    counter@3 := move ((tupled_args@2).0)
+    @4 := copy (*(counter@3)) panic.+ const (1 : u32)
+    *(counter@3) := move (@4)
+    @0 := const (true)
+    return
+}
+
+// Full name: test_crate::gives_fn::{impl FnMut<(&'_ mut (u32))> for closure}::call_mut
+fn {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_1>(@1: &'_1 mut (closure), @2: (&'_0 mut (u32))) -> bool
+{
+    let @0: bool; // return
+    let state@1: &'_1 mut (closure); // arg #1
+    let args@2: (&'_0 mut (u32)); // arg #2
+    let @3: &'_ (closure); // anonymous local
+
+    storage_live(@3)
+    @3 := &*(state@1)
+    @0 := {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_>(move (@3), move (args@2))
+    return
+}
+
+// Full name: test_crate::gives_fn::{impl FnOnce<(&'_ mut (u32))> for closure}::call_once
+fn {impl FnOnce<(&'_ mut (u32))> for closure}::call_once<'_0>(@1: closure, @2: (&'_0 mut (u32))) -> bool
+{
+    let @0: bool; // return
+    let @1: closure; // arg #1
+    let @2: (&'_ mut (u32)); // arg #2
+    let @3: &'_ mut (closure); // anonymous local
+
+    storage_live(@3)
+    @3 := &mut @1
+    @0 := {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_>(move (@3), move (@2))
+    drop[Drop<closure>] @1
+    return
+}
+
+// Full name: test_crate::gives_fn::{impl FnOnce<(&'_ mut (u32))> for closure}
+impl<'_0> FnOnce<(&'_ mut (u32))> for closure {
+    parent_clause0 = MetaSized<closure>
+    parent_clause1 = Sized<(&'_ mut (u32))>
+    parent_clause2 = Tuple<(&'_ mut (u32))>
+    parent_clause3 = Sized<bool>
+    type Output = bool
+    fn call_once = {impl FnOnce<(&'_ mut (u32))> for closure}::call_once<'_0>
+}
+
+// Full name: test_crate::gives_fn::{impl FnMut<(&'_ mut (u32))> for closure}
+impl<'_0> FnMut<(&'_ mut (u32))> for closure {
+    parent_clause0 = MetaSized<closure>
+    parent_clause1 = {impl FnOnce<(&'_ mut (u32))> for closure}<'_0>
+    parent_clause2 = Sized<(&'_ mut (u32))>
+    parent_clause3 = Tuple<(&'_ mut (u32))>
+    fn call_mut<'_0> = {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_0_0>
+}
+
+// Full name: test_crate::gives_fn::{impl Fn<(&'_ mut (u32))> for closure}
+impl<'_0> Fn<(&'_ mut (u32))> for closure {
+    parent_clause0 = MetaSized<closure>
+    parent_clause1 = {impl FnMut<(&'_ mut (u32))> for closure}<'_0>
+    parent_clause2 = Sized<(&'_ mut (u32))>
+    parent_clause3 = Tuple<(&'_ mut (u32))>
+    fn call<'_0> = {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_0_0>
+}
+
+// Full name: test_crate::gives_fn
+fn gives_fn()
+{
+    let @0: (); // return
+    let @1: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)); // anonymous local
+    let @2: &'_ (closure); // anonymous local
+    let @3: &'_ (closure); // anonymous local
+    let @4: closure; // anonymous local
+
+    storage_live(@1)
+    storage_live(@2)
+    storage_live(@3)
+    storage_live(@4)
+    @4 := closure {  }
+    @3 := &@4
+    @2 := &*(@3)
+    @1 := unsize_cast<&'_ (closure), &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)), {impl Fn<(&'_ mut (u32))> for closure}<'_>>(move (@2))
+    storage_dead(@2)
+    @0 := takes_fn<'_>(move (@1))
+    storage_dead(@1)
+    storage_dead(@4)
+    storage_dead(@3)
+    @0 := ()
+    return
+}
+
+
+
diff --git a/charon/tests/ui/simple/dyn-fn.rs b/charon/tests/ui/simple/dyn-fn.rs
new file mode 100644
index 000000000..c71ace687
--- /dev/null
+++ b/charon/tests/ui/simple/dyn-fn.rs
@@ -0,0 +1,11 @@
+fn takes_fn(f: &dyn for<'a> Fn(&'a mut u32) -> bool) {
+    let mut counter = 0;
+    if f(&mut counter) {}
+}
+
+fn gives_fn() {
+    takes_fn(&|counter| {
+        *counter += 1;
+        true
+    })
+}
diff --git a/charon/tests/ui/simple/generic-cast-to-dyn.out b/charon/tests/ui/simple/generic-cast-to-dyn.out
index 246563975..abdf997f2 100644
--- a/charon/tests/ui/simple/generic-cast-to-dyn.out
+++ b/charon/tests/ui/simple/generic-cast-to-dyn.out
@@ -31,25 +31,25 @@ pub trait Sized<Self>
 }
 
 // Full name: test_crate::foo
-fn foo<'_0, T>(@1: &'_0 (T)) -> &'_0 (dyn (exists(TODO)))
+fn foo<'_0, T>(@1: &'_0 (T)) -> &'_0 ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : 'static))
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Any<T>,
 {
-    let @0: &'_ (dyn (exists(TODO))); // return
+    let @0: &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)); // return
     let x@1: &'_ (T); // arg #1
-    let @2: &'_ (dyn (exists(TODO))); // anonymous local
-    let @3: &'_ (dyn (exists(TODO))); // anonymous local
+    let @2: &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)); // anonymous local
+    let @3: &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)); // anonymous local
     let @4: &'_ (T); // anonymous local
 
     storage_live(@2)
     storage_live(@3)
     storage_live(@4)
     @4 := &*(x@1)
-    @3 := unsize_cast<&'_ (T), &'_ (dyn (exists(TODO))), @TraitClause1>(move (@4))
+    @3 := unsize_cast<&'_ (T), &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)), @TraitClause1>(move (@4))
     storage_dead(@4)
     @2 := &*(@3)
-    @0 := unsize_cast<&'_ (dyn (exists(TODO))), &'_ (dyn (exists(TODO))), Any<dyn (exists(TODO))>>(move (@2))
+    @0 := unsize_cast<&'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)), &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)), Any<(dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)>>(move (@2))
     storage_dead(@3)
     storage_dead(@2)
     return
diff --git a/charon/tests/ui/simple/mem-discriminant-from-derive.out b/charon/tests/ui/simple/mem-discriminant-from-derive.out
index 0a6a9abb9..f2167fc4c 100644
--- a/charon/tests/ui/simple/mem-discriminant-from-derive.out
+++ b/charon/tests/ui/simple/mem-discriminant-from-derive.out
@@ -68,12 +68,6 @@ where
 // Full name: core::fmt::Error
 pub struct Error {}
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
-where
-    'a : 'a,
-
 // Full name: core::result::Result
 #[lang_item("Result")]
 pub enum Result<T, E>
diff --git a/charon/tests/ui/simple/pointee_metadata.out b/charon/tests/ui/simple/pointee_metadata.out
index e14428eff..31d835120 100644
--- a/charon/tests/ui/simple/pointee_metadata.out
+++ b/charon/tests/ui/simple/pointee_metadata.out
@@ -95,12 +95,6 @@ where
 // Full name: core::fmt::Error
 pub struct Error {}
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
-where
-    'a : 'a,
-
 // Full name: core::result::Result
 #[lang_item("Result")]
 pub enum Result<T, E>
diff --git a/charon/tests/ui/simple/ptr-from-raw-parts.out b/charon/tests/ui/simple/ptr-from-raw-parts.out
index da8df36b0..24f796331 100644
--- a/charon/tests/ui/simple/ptr-from-raw-parts.out
+++ b/charon/tests/ui/simple/ptr-from-raw-parts.out
@@ -124,12 +124,6 @@ impl Ord for () {
 // Full name: core::fmt::Error
 pub struct Error {}
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
-where
-    'a : 'a,
-
 // Full name: core::result::Result
 #[lang_item("Result")]
 pub enum Result<T, E>
diff --git a/charon/tests/ui/simple/ptr_metadata.out b/charon/tests/ui/simple/ptr_metadata.out
index 2b6d729bf..fe9e46184 100644
--- a/charon/tests/ui/simple/ptr_metadata.out
+++ b/charon/tests/ui/simple/ptr_metadata.out
@@ -124,12 +124,6 @@ impl Ord for () {
 // Full name: core::fmt::Error
 pub struct Error {}
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
-where
-    'a : 'a,
-
 // Full name: core::result::Result
 #[lang_item("Result")]
 pub enum Result<T, E>
diff --git a/charon/tests/ui/simple/slice_index_range.out b/charon/tests/ui/simple/slice_index_range.out
index b6a93613d..21480671a 100644
--- a/charon/tests/ui/simple/slice_index_range.out
+++ b/charon/tests/ui/simple/slice_index_range.out
@@ -3,23 +3,6 @@
 // Full name: core::fmt::Error
 pub struct Error {}
 
-// Full name: core::fmt::FormattingOptions
-pub struct FormattingOptions {
-  flags: u32,
-  width: u16,
-  precision: u16,
-}
-
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub struct Formatter<'a>
-where
-    'a : 'a,
-{
-  options: FormattingOptions,
-  buf: &'a mut (dyn (exists(TODO))),
-}
-
 // Full name: core::marker::MetaSized
 #[lang_item("meta_sized")]
 pub trait MetaSized<Self>
diff --git a/charon/tests/ui/string-literal.out b/charon/tests/ui/string-literal.out
index 44c5985d1..f8030f1c6 100644
--- a/charon/tests/ui/string-literal.out
+++ b/charon/tests/ui/string-literal.out
@@ -3,12 +3,6 @@
 // Full name: core::fmt::Error
 pub struct Error {}
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
-where
-    'a : 'a,
-
 // Full name: core::marker::MetaSized
 #[lang_item("meta_sized")]
 pub trait MetaSized<Self>
diff --git a/charon/tests/ui/type_inference_is_order_dependent.out b/charon/tests/ui/type_inference_is_order_dependent.out
index 96eb0a786..c26cd4648 100644
--- a/charon/tests/ui/type_inference_is_order_dependent.out
+++ b/charon/tests/ui/type_inference_is_order_dependent.out
@@ -36,12 +36,6 @@ impl Default for bool {
 // Full name: core::fmt::Error
 pub struct Error {}
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
-where
-    'a : 'a,
-
 // Full name: core::fmt::Arguments
 #[lang_item("format_arguments")]
 pub opaque type Arguments<'a>
diff --git a/charon/tests/ui/unsafe.out b/charon/tests/ui/unsafe.out
index 64a3dae6a..5e72cd220 100644
--- a/charon/tests/ui/unsafe.out
+++ b/charon/tests/ui/unsafe.out
@@ -124,12 +124,6 @@ impl Ord for () {
 // Full name: core::fmt::Error
 pub struct Error {}
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
-where
-    'a : 'a,
-
 // Full name: core::result::Result
 #[lang_item("Result")]
 pub enum Result<T, E>
diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out
index e1e9543ee..67e135068 100644
--- a/charon/tests/ui/unsize.out
+++ b/charon/tests/ui/unsize.out
@@ -27,12 +27,6 @@ where
 // Full name: core::fmt::Error
 pub struct Error {}
 
-// Full name: core::fmt::Formatter
-#[lang_item("Formatter")]
-pub opaque type Formatter<'a>
-where
-    'a : 'a,
-
 // Full name: core::result::Result
 #[lang_item("Result")]
 pub enum Result<T, E>
@@ -169,14 +163,14 @@ fn foo()
     let @9: Rc<Array<i32, 2 : usize>>[MetaSized<Array<i32, 2 : usize>>, Sized<Global>]; // anonymous local
     let @10: Array<i32, 2 : usize>; // anonymous local
     let string@11: String; // local
-    let @12: &'_ (dyn (exists(TODO))); // anonymous local
+    let @12: &'_ ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)); // anonymous local
     let @13: &'_ (String); // anonymous local
     let @14: &'_ (String); // anonymous local
-    let @15: alloc::boxed::Box<dyn (exists(TODO))>[MetaSized<dyn (exists(TODO))>, Sized<Global>]; // anonymous local
+    let @15: alloc::boxed::Box<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized<Global>]; // anonymous local
     let @16: alloc::boxed::Box<String>[MetaSized<String>, Sized<Global>]; // anonymous local
     let @17: String; // anonymous local
     let @18: &'_ (String); // anonymous local
-    let @19: Rc<dyn (exists(TODO))>[MetaSized<dyn (exists(TODO))>, Sized<Global>]; // anonymous local
+    let @19: Rc<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized<Global>]; // anonymous local
     let @20: Rc<String>[MetaSized<String>, Sized<Global>]; // anonymous local
     let @21: String; // anonymous local
     let @22: &'_ (String); // anonymous local
@@ -221,7 +215,7 @@ fn foo()
     storage_live(@14)
     @14 := &string@11
     @13 := &*(@14)
-    @12 := unsize_cast<&'_ (String), &'_ (dyn (exists(TODO))), {impl Display for String}>(move (@13))
+    @12 := unsize_cast<&'_ (String), &'_ ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)), {impl Display for String}>(move (@13))
     storage_dead(@13)
     storage_dead(@14)
     storage_dead(@12)
@@ -233,11 +227,11 @@ fn foo()
     @17 := {impl Clone for String}::clone<'_>(move (@18))
     storage_dead(@18)
     @16 := @BoxNew<String>[Sized<String>](move (@17))
-    @15 := unsize_cast<alloc::boxed::Box<String>[MetaSized<String>, Sized<Global>], alloc::boxed::Box<dyn (exists(TODO))>[MetaSized<dyn (exists(TODO))>, Sized<Global>], {impl Display for String}>(move (@16))
+    @15 := unsize_cast<alloc::boxed::Box<String>[MetaSized<String>, Sized<Global>], alloc::boxed::Box<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized<Global>], {impl Display for String}>(move (@16))
     drop[{impl Drop for alloc::boxed::Box<T>[@TraitClause0, @TraitClause1]}<String, Global>[MetaSized<String>, Sized<Global>]] @16
     storage_dead(@17)
     storage_dead(@16)
-    drop[{impl Drop for alloc::boxed::Box<T>[@TraitClause0, @TraitClause1]}<dyn (exists(TODO)), Global>[MetaSized<dyn (exists(TODO))>, Sized<Global>]] @15
+    drop[{impl Drop for alloc::boxed::Box<T>[@TraitClause0, @TraitClause1]}<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_), Global>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized<Global>]] @15
     storage_dead(@15)
     storage_live(@19)
     storage_live(@20)
@@ -247,11 +241,11 @@ fn foo()
     @21 := {impl Clone for String}::clone<'_>(move (@22))
     storage_dead(@22)
     @20 := alloc::rc::{Rc<T>[@TraitClause0::parent_clause0, Sized<Global>]}::new<String>[Sized<String>](move (@21))
-    @19 := unsize_cast<Rc<String>[MetaSized<String>, Sized<Global>], Rc<dyn (exists(TODO))>[MetaSized<dyn (exists(TODO))>, Sized<Global>]>(move (@20))
+    @19 := unsize_cast<Rc<String>[MetaSized<String>, Sized<Global>], Rc<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized<Global>]>(move (@20))
     drop[{impl Drop for Rc<T>[@TraitClause0, @TraitClause1]}<String, Global>[MetaSized<String>, Sized<Global>]] @20
     storage_dead(@21)
     storage_dead(@20)
-    drop[{impl Drop for Rc<T>[@TraitClause0, @TraitClause1]}<dyn (exists(TODO)), Global>[MetaSized<dyn (exists(TODO))>, Sized<Global>]] @19
+    drop[{impl Drop for Rc<T>[@TraitClause0, @TraitClause1]}<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_), Global>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized<Global>]] @19
     storage_dead(@19)
     @0 := ()
     drop[{impl Drop for String}] string@11