diff --git a/src/type_system/tests/subtyping/liskov/cancellation.rs b/src/type_system/tests/subtyping/liskov/cancellation.rs
index 0c788f9..f638b3e 100644
--- a/src/type_system/tests/subtyping/liskov/cancellation.rs
+++ b/src/type_system/tests/subtyping/liskov/cancellation.rs
@@ -574,9 +574,9 @@ fn c4_shared_d1d2d3_not_subtype_of_shared_d1_shared_d2d3() {
 }
 
 #[test]
-fn c4_leased_d1d2d3_not_subtype_of_leased_d1_leased_d2d3() {
-    // This one fails because (a) you can only cancel `leased` if it is leased from something else
-    // and (b) the supertype includes a chain `leased[d2] Data` which is not a subtype of `leased[d1]` Data.
+fn c4_leased_d1d2d3_subtype_of_leased_d1_leased_d2d3() {
+    // This one succeeds because `leased[d1, d2, d3]` and `leased[d1] leased[d2, d3]` are
+    // equivalent. Leased steps in the chain are unioned.
     check_program(&term(
         "
         class Data { }
@@ -591,56 +591,7 @@ fn c4_leased_d1d2d3_not_subtype_of_leased_d1_leased_d2d3() {
         }
         ",
     ))
-    .assert_err(expect_test::expect![[r#"
-        check program `class Data { } class Main { fn test [perm] (my self) -> () { let d1 : my Data = new Data () ; let d2 : my Data = new Data () ; let d3 : my Data = new Data () ; let s1 : leased [d1, d2, d3] Data = d1 . lease ; let s2 : leased [d1] leased [d2, d3] Data = s1 . give ; } }`
-
-        Caused by:
-            0: check class named `Main`
-            1: check method named `test`
-            2: check function body
-            3: judgment `can_type_expr_as { expr: { let d1 : my Data = new Data () ; let d2 : my Data = new Data () ; let d3 : my Data = new Data () ; let s1 : leased [d1, d2, d3] Data = d1 . lease ; let s2 : leased [d1] leased [d2, d3] Data = s1 . give ; }, as_ty: (), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                 the rule "can_type_expr_as" failed at step #0 (src/file.rs:LL:CC) because
-                   judgment `type_expr_as { expr: { let d1 : my Data = new Data () ; let d2 : my Data = new Data () ; let d3 : my Data = new Data () ; let s1 : leased [d1, d2, d3] Data = d1 . lease ; let s2 : leased [d1] leased [d2, d3] Data = s1 . give ; }, as_ty: (), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                     the rule "type_expr_as" failed at step #0 (src/file.rs:LL:CC) because
-                       judgment `type_expr { expr: { let d1 : my Data = new Data () ; let d2 : my Data = new Data () ; let d3 : my Data = new Data () ; let s1 : leased [d1, d2, d3] Data = d1 . lease ; let s2 : leased [d1] leased [d2, d3] Data = s1 . give ; }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                         the rule "block" failed at step #0 (src/file.rs:LL:CC) because
-                           judgment `type_block { block: { let d1 : my Data = new Data () ; let d2 : my Data = new Data () ; let d3 : my Data = new Data () ; let s1 : leased [d1, d2, d3] Data = d1 . lease ; let s2 : leased [d1] leased [d2, d3] Data = s1 . give ; }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                             the rule "place" failed at step #0 (src/file.rs:LL:CC) because
-                               judgment `type_statements_with_final_ty { statements: [let d1 : my Data = new Data () ;, let d2 : my Data = new Data () ;, let d3 : my Data = new Data () ;, let s1 : leased [d1, d2, d3] Data = d1 . lease ;, let s2 : leased [d1] leased [d2, d3] Data = s1 . give ;], ty: (), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                                 the rule "cons" failed at step #2 (src/file.rs:LL:CC) because
-                                   judgment `type_statements_with_final_ty { statements: [let d2 : my Data = new Data () ;, let d3 : my Data = new Data () ;, let s1 : leased [d1, d2, d3] Data = d1 . lease ;, let s2 : leased [d1] leased [d2, d3] Data = s1 . give ;], ty: (), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                                     the rule "cons" failed at step #2 (src/file.rs:LL:CC) because
-                                       judgment `type_statements_with_final_ty { statements: [let d3 : my Data = new Data () ;, let s1 : leased [d1, d2, d3] Data = d1 . lease ;, let s2 : leased [d1] leased [d2, d3] Data = s1 . give ;], ty: (), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                                         the rule "cons" failed at step #2 (src/file.rs:LL:CC) because
-                                           judgment `type_statements_with_final_ty { statements: [let s1 : leased [d1, d2, d3] Data = d1 . lease ;, let s2 : leased [d1] leased [d2, d3] Data = s1 . give ;], ty: (), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                                             the rule "cons" failed at step #2 (src/file.rs:LL:CC) because
-                                               judgment `type_statements_with_final_ty { statements: [let s2 : leased [d1] leased [d2, d3] Data = s1 . give ;], ty: (), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                                                 the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
-                                                   judgment `type_statement { statement: let s2 : leased [d1] leased [d2, d3] Data = s1 . give ;, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                                                     the rule "let" failed at step #0 (src/file.rs:LL:CC) because
-                                                       judgment `type_expr_as { expr: s1 . give, as_ty: leased [d1] leased [d2, d3] Data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                                                         the rule "type_expr_as" failed at step #1 (src/file.rs:LL:CC) because
-                                                           judgment `sub { a: leased [d1, d2, d3] Data, b: leased [d1] leased [d2, d3] Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
-                                                             the rule "sub" failed at step #0 (src/file.rs:LL:CC) because
-                                                               judgment `sub_in_cx { cx_a: my, a: leased [d1, d2, d3] Data, cx_b: my, b: leased [d1] leased [d2, d3] Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
-                                                                 the rule "sub" failed at step #2 (src/file.rs:LL:CC) because
-                                                                   judgment `sub_ty_chain_sets { ty_liens_a: {ClassTy(leased[d1], Data), ClassTy(leased[d2], Data), ClassTy(leased[d3], Data)}, ty_liens_b: {ClassTy(leased[d1] leased[d2], Data), ClassTy(leased[d1] leased[d3], Data)}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
-                                                                     the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
-                                                                       judgment `sub_ty_chains { ty_chain_a: ClassTy(leased[d1], Data), ty_chain_b: ClassTy(leased[d1] leased[d2], Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
-                                                                         the rule "class ty" failed at step #4 (src/file.rs:LL:CC) because
-                                                                           judgment `sub_lien_chains { a: leased[d1], b: leased[d1] leased[d2], live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
-                                                                             the rule "cancel leased" failed at step #0 (src/file.rs:LL:CC) because
-                                                                               judgment had no applicable rules: `lien_chain_is_leased { chain: my, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`
-                                                                             the rule "matched starts" failed at step #1 (src/file.rs:LL:CC) because
-                                                                               judgment had no applicable rules: `extension_covered_by { a: my, b: leased[d2], env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`
-                                                                     the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
-                                                                       judgment `sub_ty_chains { ty_chain_a: ClassTy(leased[d1], Data), ty_chain_b: ClassTy(leased[d1] leased[d3], Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
-                                                                         the rule "class ty" failed at step #4 (src/file.rs:LL:CC) because
-                                                                           judgment `sub_lien_chains { a: leased[d1], b: leased[d1] leased[d3], live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
-                                                                             the rule "cancel leased" failed at step #0 (src/file.rs:LL:CC) because
-                                                                               judgment had no applicable rules: `lien_chain_is_leased { chain: my, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`
-                                                                             the rule "matched starts" failed at step #1 (src/file.rs:LL:CC) because
-                                                                               judgment had no applicable rules: `extension_covered_by { a: my, b: leased[d3], env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: my Data, d2: my Data, d3: my Data, s1: leased [d1, d2, d3] Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`"#]]);
+    .assert_ok(expect_test::expect!["()"]);
 }
 
 #[test]