diff --git a/crates/ailang-check/tests/workspace.rs b/crates/ailang-check/tests/workspace.rs
index 0b46754..e3d86eb 100644
--- a/crates/ailang-check/tests/workspace.rs
+++ b/crates/ailang-check/tests/workspace.rs
@@ -725,7 +725,7 @@ fn borrow_own_demo_is_linearity_clean() {
 /// is active today) and were RED before the hardening (docs/specs/0063).
 #[test]
 fn harden_ownership_false_positives_are_clean() {
-    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof", "c2_let_alias"] {
+    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof", "c2_let_alias", "c4_rewrite"] {
         let entry = examples_dir().join(format!("{name}.ail"));
         let ws = load_workspace(&entry).unwrap_or_else(|e| panic!("load {name}: {e:?}"));
         let diags = check_workspace(&ws);
@@ -737,19 +737,23 @@ fn harden_ownership_false_positives_are_clean() {
     }
 }
 
-/// #56 type-gating: the exemption is value-type-only. A heap param
-/// consumed twice (`real_consume.dup`, `(term-ctor Pair Pair b b)`) MUST
-/// still fire use-after-consume — proving the fix did not blanket-silence
-/// genuine multi-consume.
+/// #56 type-gating + #57 class 4: a heap value consumed twice MUST still
+/// fire use-after-consume — `real_consume.dup` (`(term-ctor Pair Pair b
+/// b)`) and `c4_double_consume.both` (`rest` projected by both `fst` and
+/// `snd`, the genuine double-consume the partition_eithers rewrite
+/// removes). Proves the hardening did not blanket-silence genuine
+/// multi-consume.
 #[test]
 fn harden_ownership_heap_double_consume_still_errors() {
-    let entry = examples_dir().join("real_consume.ail");
-    let ws = load_workspace(&entry).expect("load real_consume");
-    let diags = check_workspace(&ws);
-    assert!(
-        diags.iter().any(|d| d.code == "use-after-consume"),
-        "real_consume.dup must still fire use-after-consume; got: {diags:#?}"
-    );
+    for name in ["real_consume", "c4_double_consume"] {
+        let entry = examples_dir().join(format!("{name}.ail"));
+        let ws = load_workspace(&entry).unwrap_or_else(|e| panic!("load {name}: {e:?}"));
+        let diags = check_workspace(&ws);
+        assert!(
+            diags.iter().any(|d| d.code == "use-after-consume"),
+            "{name} must still fire use-after-consume; got: {diags:#?}"
+        );
+    }
 }
 
 /// RED for fieldtest finding B1 (docs/specs/0058): reading a
diff --git a/examples/c4_double_consume.ail b/examples/c4_double_consume.ail
new file mode 100644
index 0000000..638bc41
--- /dev/null
+++ b/examples/c4_double_consume.ail
@@ -0,0 +1,13 @@
+(module c4_double_consume
+  (data Pair
+    (doc "boxed pair of ints")
+    (ctor MkPair (con Int) (con Int)))
+  (fn fst (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p)
+    (body (match p (case (pat-ctor MkPair a b) a))))
+  (fn snd (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p)
+    (body (match p (case (pat-ctor MkPair a b) b))))
+  (fn both
+    (doc "MUST STAY RED: rest projected by fst AND snd = consumed twice")
+    (type (fn-type (params (own (con Pair))) (ret (own (con Pair)))))
+    (params rest)
+    (body (term-ctor Pair MkPair (app fst rest) (app snd rest)))))
diff --git a/examples/c4_rewrite.ail b/examples/c4_rewrite.ail
new file mode 100644
index 0000000..2dc0d81
--- /dev/null
+++ b/examples/c4_rewrite.ail
@@ -0,0 +1,9 @@
+(module c4_rewrite
+  (data Pair
+    (doc "boxed pair of ints")
+    (ctor MkPair (con Int) (con Int)))
+  (fn both
+    (doc "rewrite: destructure rest once via match")
+    (type (fn-type (params (own (con Pair))) (ret (own (con Pair)))))
+    (params rest)
+    (body (match rest (case (pat-ctor MkPair a b) (term-ctor Pair MkPair a b))))))
diff --git a/examples/std_either_list.ail b/examples/std_either_list.ail
index df4deeb..b883584 100644
--- a/examples/std_either_list.ail
+++ b/examples/std_either_list.ail
@@ -45,7 +45,7 @@
         (case _ (term-ctor List Nil)))))
 
   (fn partition_eithers
-    (doc "Partition a list of Eithers into a Pair<List<e>, List<a>>: lefts on the left, rights on the right. Single pass via direct recursion; head dispatch is a flat match on the recursive result's projections.")
+    (doc "Partition a list of Eithers into a Pair<List<e>, List<a>>: lefts on the left, rights on the right. Single pass via direct recursion; the recursive result is destructured once and the head dispatches into the matching side.")
     (type
       (forall (vars e a)
         (fn-type
@@ -60,12 +60,14 @@
             (term-ctor List Nil)))
         (case (pat-ctor Cons h t)
           (let rest (app partition_eithers t)
-            (match h
-              (case (pat-ctor Left l)
-                (term-ctor Pair MkPair
-                  (term-ctor List Cons l (app Pair.fst rest))
-                  (app Pair.snd rest)))
-              (case (pat-ctor Right r)
-                (term-ctor Pair MkPair
-                  (app Pair.fst rest)
-                  (term-ctor List Cons r (app Pair.snd rest)))))))))))
+            (match rest
+              (case (pat-ctor MkPair ls rs)
+                (match h
+                  (case (pat-ctor Left l)
+                    (term-ctor Pair MkPair
+                      (term-ctor List Cons l ls)
+                      rs))
+                  (case (pat-ctor Right r)
+                    (term-ctor Pair MkPair
+                      ls
+                      (term-ctor List Cons r rs))))))))))))