diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index d9a604b..0c74973 100644
--- a/model_with_structures/analyzer.ml
+++ b/model_with_structures/analyzer.ml
@@ -459,7 +459,7 @@ struct
       | TupleV vs, TupleT ts -> ignore @@ List.map2 (tags_check mem) vs ts
       | _, _ -> raise @@ Typing_error "tags_check"
 
-  (* - writable type *)
+  (* - writability check *)
 
   let rec is_all_type_writable (t : atype) : bool =
     match t with
diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 3f21ae3..937a1f5 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -1471,21 +1471,10 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 
 #h(10pt)
 
-=== Writable Type
+=== Writability Check
 
 #let twrite = $attach(tack.r, br: #[`write`])$
 
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ writable unit type: MaybeWrite],
-
-    $twrite cl r, MaybeWrite cr$,
-  )
-))
-
-#h(10pt)
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -1500,7 +1489,18 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ writable  ref type],
+    name: [ writable unit type: MaybeWrite],
+
+    $twrite cl r, MaybeWrite cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ writable ref type],
 
     $twrite t$,
     $twrite rf c space t$,
diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml
index 7a61927..19a93e2 100644
--- a/model_with_structures/synthesizer.ml
+++ b/model_with_structures/synthesizer.ml
@@ -1158,7 +1158,7 @@ struct
         List.mapo (tags_checko mem) vs tps }
   }
 
-  (* - writable type *)
+  (* - writability check *)
 
   let rec is_all_type_writableo tp =
     let open Type in