diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 3d4398a37aebaa8d4173d8cf9f2f62af2ac65c6e..c282642773ed0f0fe012275a7862edafc9383c8a 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -8,7 +8,7 @@ Section typing.
   Context `{typeG Σ}.
 
   (** Jumping to and defining a continuation. *)
-  Lemma type_jump E L C T k args T' :
+  Lemma type_jump args E L C T k T' :
     (k ◁cont(L, T'))%CC ∈ C →
     tctx_incl E L T (T' (list_to_vec args)) →
     typed_body E L C T (k (of_val <$> args)).
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 7211456e1e2501f19c35c39be1c1e3af7889bad9..22a3cd2726f213b7bdf2e8ea30e4b4de91bcbb8a 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -235,9 +235,9 @@ Section typing.
   Qed.
 
   Lemma type_letalloc_1 {E L} ty C T T' (x : string) p e :
-    ty.(ty_size) = 1%nat →
     Closed [] p → Closed (x :b: []) e →
     tctx_extract_hasty E L p ty T T' →
+    ty.(ty_size) = 1%nat →
     (∀ (v : val), typed_body E L C ((v ◁ own 1 ty)::T') (subst x v e)) →
     typed_body E L C T (letalloc: x := p in e).
   Proof.
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index 61ba2c297d6e59e1bd3e9419ddea226b378395fe..cc8982e4b4d5f8f82a18052ed4d16ec74b6e91aa 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -23,6 +23,6 @@ Section get_x.
       intros p'; simpl_subst.
     eapply (type_letalloc_1 (&shr{α}int)); (try solve_typing)=>r. simpl_subst.
     eapply type_delete; try solve_typing.
-    eapply type_jump with (args := [r]); solve_typing.
+    eapply (type_jump [_]); solve_typing.
   Qed.
 End get_x.
diff --git a/theories/typing/tests/rebor.v b/theories/typing/tests/rebor.v
new file mode 100644
index 0000000000000000000000000000000000000000..cae48c5a029b2629fb8080d6dcae0a7695320695
--- /dev/null
+++ b/theories/typing/tests/rebor.v
@@ -0,0 +1,41 @@
+From lrust.lifetime Require Import definitions.
+From lrust.lang Require Import new_delete.
+From lrust.typing Require Import programs product product_split own uniq_bor
+                    shr_bor int function lft_contexts uninit cont borrow.
+Set Default Proof Using "Type".
+
+Section rebor.
+  Context `{typeG Σ}.
+
+  Definition rebor :=
+    (funrec: <> ["t1"; "t2"] :=
+       Newlft;;
+       letalloc: "x" := "t1" in
+       let: "x'" := !"x" in let: "y" := "x'" +â‚— #0 in
+       "x" <- "t2";;
+       let: "y'" := !"y" in
+       letalloc: "r" := "y'" in
+       Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
+                 delete [ #1; "x"] ;; "return" ["r":expr])%E.
+
+  Lemma rebor_type :
+    typed_instruction_ty [] [] [] rebor
+        (fn (λ _, []) (λ _, [# own 2 (Π[int; int]); own 2 (Π[int; int])])
+            (λ (_ : ()), own 1 int)).
+  Proof.
+    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>t1 t2. simpl_subst.
+    eapply (type_newlft []). apply _. move=> α.
+    eapply (type_letalloc_1 (&uniq{α}Π[int; int])); (try solve_typing)=>x. simpl_subst.
+    eapply type_deref; try solve_typing; [apply read_own_move|done|]=>x'. simpl_subst.
+    eapply (type_letpath (&uniq{α}int)); (try solve_typing)=>y. simpl_subst.
+    eapply (type_assign _ (&uniq{α}Π [int; int])); try solve_typing. by apply write_own.
+    eapply type_deref; try solve_typing; [apply: read_uniq; solve_typing|done|]=>y'.
+      simpl_subst.
+    eapply type_letalloc_1; (try solve_typing)=>r. simpl_subst.
+    eapply type_endlft; try solve_typing.
+    eapply type_delete; try solve_typing.
+    eapply type_delete; try solve_typing.
+    eapply type_delete; try solve_typing.
+    eapply (type_jump [_]); solve_typing.
+  Qed.
+End rebor.