diff --git a/theories/typing/unsafe/refcell/ref.v b/theories/typing/unsafe/refcell/ref.v
index 9e9f8c0afc53e9e71a3ea7970cfd97f05365ff48..0d8000a697a87b793a713dd93b321bd1d96cd62b 100644
--- a/theories/typing/unsafe/refcell/ref.v
+++ b/theories/typing/unsafe/refcell/ref.v
@@ -11,6 +11,14 @@ Definition refcell_refN := refcellN .@ "ref".
 Section ref.
   Context `{typeG Σ, refcellG Σ}.
 
+  (* The Rust type looks as follows (after some unfolding):
+
+     pub struct Ref<'b, T: ?Sized + 'b> {
+       value: &'b T,
+       borrow: &'b Cell<BorrowFlag>,
+     }
+  *)
+
   Program Definition ref (α : lft) (ty : type) :=
     {| ty_size := 2;
        ty_own tid vl :=
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index 0eb1bb4deec190ecfa221bddd3f94e31d946efbe..1f30af14da1415e4d1da258d6f063197201c2f3a 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -83,6 +83,13 @@ End refcell_inv.
 Section refcell.
   Context `{typeG Σ, refcellG Σ}.
 
+  (* Original Rust type:
+     pub struct RefCell<T: ?Sized> {
+       borrow: Cell<BorrowFlag>,
+       value: UnsafeCell<T>,
+     }
+  *)
+
   Program Definition refcell (ty : type) :=
     {| ty_size := S ty.(ty_size);
        ty_own tid vl :=
diff --git a/theories/typing/unsafe/refcell/refmut.v b/theories/typing/unsafe/refcell/refmut.v
index 36a86ad35098fe05ccc1638eaa6f1e23d9106bd6..df19723ee7a97539fdc51ae3fe37c1a91fc4e071 100644
--- a/theories/typing/unsafe/refcell/refmut.v
+++ b/theories/typing/unsafe/refcell/refmut.v
@@ -9,6 +9,16 @@ Set Default Proof Using "Type".
 Section refmut.
   Context `{typeG Σ, refcellG Σ}.
 
+  (* The Rust type looks as follows (after some unfolding):
+
+     pub struct RefMut<'b, T: ?Sized + 'b> {
+       value: &'b mut T,
+       borrow: &'b Cell<BorrowFlag>,
+     }
+
+     In other words, we have a pointer to the data, and a pointer
+     to the refcount field of the RefCell. *)
+
   Program Definition refmut (α : lft) (ty : type) :=
     {| ty_size := 2;
        ty_own tid vl :=
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 61efe2a71f737e382b2c697322135f84c7fe9cbb..3b67b964b68148ebfcefea1bba782d9fe1d9e3ac 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -173,7 +173,7 @@ Section refmut_functions.
   Lemma refmut_map_type ty1 ty2 envty E :
     typed_instruction_ty [] [] [] refmut_map
       (fn(∀ β, [☀β] ++ E; refmut β ty1,
-                          fn(∀ α, [☀α] ++ E; envty, &uniq{α}ty1) → &uniq{α}ty2,
+                          fn(∀ α, [☀α] ++ E; envty, &uniq{α} ty1) → &uniq{α} ty2,
                           envty)
        → refmut β ty2).
   Proof.