diff --git a/theories/rust_typing/automation.v b/theories/rust_typing/automation.v
index a22ffcc71d52738cc092a19be94422670f288ceb..951ed3b2c50b22f1b12282c0b7b5b3bf1f727537 100644
--- a/theories/rust_typing/automation.v
+++ b/theories/rust_typing/automation.v
@@ -752,9 +752,9 @@ Section tac.
            in
       let E := ((fp.2 κs tys x).(fp_elctx) ϝ) in
       let L := [ϝ ⊑ₗ{0} []] in
-      ∃ E' E'', ⌜E = E'⌝ ∗ ⌜E' ≡ₚ E''⌝ ∗
-      (credit_store 0 0 -∗ introduce_with_hooks E'' L (Qinit) (λ L2,
-        introduce_typed_stmt π E'' L2 ϝ fn lsa lsv lya lyv (
+      ∃ E', ⌜E' ⊆+ E⌝ ∗
+      (credit_store 0 0 -∗ introduce_with_hooks E' L (Qinit) (λ L2,
+        introduce_typed_stmt π E' L2 ϝ fn lsa lsv lya lyv (
         λ v L2,
             prove_with_subtype E L2 false ProveDirect (fn_ret_prop π (fp.2 κs tys x).(fp_fr) v) (λ L3 _ R3,
             introduce_with_hooks E L3 R3 (λ L4,
@@ -773,8 +773,8 @@ Section tac.
     iIntros (?) "#CTX #HE HL Hna Hcont".
     iApply fupd_wps.
     iPoseProof ("Ha" with "Hx1 Hx2") as "HT".
-    iDestruct ("HT" $! lsa lsv) as "(%E' & %E'' & <- & %Heq & HT)".
-    iPoseProof (elctx_interp_permut with "HE") as "HE'". { symmetry. apply Heq. }
+    iDestruct ("HT" $! lsa lsv) as "(%E' & %Hsub & HT)".
+    iPoseProof (elctx_interp_submseteq _ _ Hsub with "HE") as "HE'".
     rewrite /introduce_with_hooks.
     iMod ("HT" with "Hstore [] HE' HL [Hinit]") as "(%L2 & HL & HT)"; first done.
     { iDestruct "Hinit" as "($ & $ & $)". }
@@ -805,9 +805,8 @@ Tactic Notation "start_function" constr(fnname) ident(ϝ) "(" simple_intropatter
     let lsa := fresh "lsa" in let lsv := fresh "lsv" in
     iIntros (lsa lsv);
     prepare_initial_coq_context;
-    iExists _, _; iSplitR;
-    [iPureIntro; solve [simplify_elctx] | ];
-    iSplitR; [iPureIntro; solve[reorder_elctx] | ];
+    iExists _; iSplitR;
+    [iPureIntro; solve [preprocess_elctx] | ];
     inv_vec lsv; inv_vec lsa;
     simpl; unfold typarams_wf, typaram_wf;
     init_cache
diff --git a/theories/rust_typing/automation/solvers.v b/theories/rust_typing/automation/solvers.v
index 8f7534a560fcdb4a67bb884fddd12458ac29b6cb..f98ca0861e96b5e868c8e9df581ca30de6f18c5e 100644
--- a/theories/rust_typing/automation/solvers.v
+++ b/theories/rust_typing/automation/solvers.v
@@ -339,7 +339,7 @@ Section incl_tac.
     rewrite lft_intersect_list_app.
     rewrite lft_intersect_comm. done.
   Qed.
-  Lemma lctx_lft_incl_list_intersect_l E L κs1 κs2 κs i P : 
+  Lemma lctx_lft_incl_list_intersect_l E L κs1 κs2 κs i P :
     κs1 !! i = Some (lft_intersect_list κs) →
     lctx_lft_incl_list E L (delete i κs1 ++ κs) κs2 ∨ P →
     lctx_lft_incl_list E L κs1 κs2 ∨ P.
@@ -351,7 +351,7 @@ Section incl_tac.
     move: Ha.
     rewrite !lft_intersect_list_app. simpl.
     rewrite [lft_intersect_list κs ⊓ lft_intersect_list (drop _ _)]lft_intersect_comm.
-    rewrite lft_intersect_assoc. 
+    rewrite lft_intersect_assoc.
     done.
   Qed.
 
@@ -407,7 +407,10 @@ Section incl_external_tac.
   Proof. done. Qed.
 
   (* Pick an expansion *)
-  (* TODO: why don't I expand from the RHS, and then only expand the head lft, one by one? *)
+  (* We also expand from the LHS, as we expand local lifetimes from the LHS.
+     Expanding external lifetimes from the RHS would make some goals unprovable, e.g.
+      [lctx_lft_incl [κ ⊑ₑ κ'] [κ' ⊑ₗ{ c1} [κ'']] κ κ'']
+  *)
   Lemma tac_lctx_lft_incl_list_expand_ext_choose E L (e1 c1 : lft) candidates κs1 κs2 i P :
     (e1 ⊑ₑ c1) ∈ E →
     κs1 !! i = Some e1 →
@@ -1193,6 +1196,63 @@ Ltac reorder_elctx :=
       | rewrite ?app_nil_r; reflexivity ]
   end.
 
+(* TODO eliminate cyclic external inclusions *)
+
+(** Optimize an elctx by removing unnecessary inclusions *)
+Section optimize_elctx.
+  Context `{!typeGS Σ}.
+
+  Lemma tac_optimize_elctx_remove (E E' : elctx) κ κ' :
+    E' ⊆+ E →
+    E' ⊆+ (κ ⊑ₑ κ') :: E.
+  Proof.
+    intros ->. by apply submseteq_cons.
+  Qed.
+  Lemma tac_optimize_elctx_keep (E E' E'' : elctx) κ κ' :
+    E' = (κ ⊑ₑ κ') :: E'' →
+    E'' ⊆+ E →
+    E' ⊆+ (κ ⊑ₑ κ') :: E.
+  Proof.
+    intros ->. by apply submseteq_skip.
+  Qed.
+  Lemma tac_optimize_elctx_finish (E E' : elctx) :
+    E' = E →
+    E' ⊆+ E.
+  Proof. by intros ->. Qed.
+End optimize_elctx.
+
+Ltac optimize_elctx_step :=
+  lazymatch goal with
+  | |- ?E' ⊆+ (?κ ⊑ₑ ?κ) :: ?E =>
+      notypeclasses refine (tac_optimize_elctx_remove _ _ _ _ _)
+  | |- ?E' ⊆+ (?κ ⊑ₑ ?κ') :: ?E =>
+      notypeclasses refine (tac_optimize_elctx_keep _ _ _ _ _ _ _);
+      [ reflexivity | ]
+  | |- ?E' ⊆+ _ =>
+      notypeclasses refine (tac_optimize_elctx_finish _ _ _);
+      reflexivity
+  end.
+Ltac optimize_elctx :=
+  repeat optimize_elctx_step.
+
+(** Combined elctx preprocessing *)
+Lemma tac_preprocess_elctx (E1 E2 E E' : elctx) :
+  E = E1 →
+  E1 ≡ₚ E2 →
+  E' ⊆+ E2 →
+  E' ⊆+ E.
+Proof.
+  intros -> ->. done.
+Qed.
+
+Ltac preprocess_elctx :=
+  match goal with
+  | |- ?E' ⊆+ ?E =>
+      notypeclasses refine (tac_preprocess_elctx _ _ _ _ _ _ _);
+      [simplify_elctx | reorder_elctx | optimize_elctx]
+  end.
+
+
 (** elctx_sat solver *)
 Section elctx_sat.
   Context `{typeGS Σ}.
diff --git a/theories/rust_typing/lft_contexts.v b/theories/rust_typing/lft_contexts.v
index 5ec899d026fada17d77d8d92bb7ea53623d82a1e..7c123b85861216997209d2848d56dabc4dce406e 100644
--- a/theories/rust_typing/lft_contexts.v
+++ b/theories/rust_typing/lft_contexts.v
@@ -89,6 +89,15 @@ Section lft_contexts.
     Persistent (elctx_interp E).
   Proof. apply _. Qed.
 
+  Lemma elctx_interp_submseteq E E' :
+    E' ⊆+ E →
+    elctx_interp E -∗
+    elctx_interp E'.
+  Proof.
+    rewrite /elctx_interp.
+    iIntros (?) "Ha". iApply big_sepL_submseteq; done.
+  Qed.
+
   (* Local lifetime contexts. *)
   (** The fraction_map for [κ] is stored at [γ]. *)
   Definition lft_has_gname_def (κ : lft) (γ : gname) : iProp Σ :=
@@ -475,6 +484,17 @@ Section lft_contexts.
     iApply lft_incl_refl.
   Qed.
 
+  Lemma lctx_lft_incl_external_full_r κ1 κ2 κ κ' :
+    κ2 ⊑ₑ κ1 ∈ E → lctx_lft_incl κ (κ2 ⊓ κ') → lctx_lft_incl κ (κ1 ⊓ κ').
+  Proof.
+    intros Hin Hincl. etrans; first done.
+    iIntros (?) "HL". iPoseProof (Hincl with "HL") as "#Hincl".
+    iIntros "!>#HE". iDestruct ("Hincl" with "HE") as "#?".
+    iApply lft_intersect_mono; last iApply lft_incl_refl.
+    iDestruct (big_sepL_elem_of with "HE") as "#Hincl'"; first done.
+    done.
+  Qed.
+
   Lemma lctx_lft_incl_external κ κ' : κ ⊑ₑ κ' ∈ E → lctx_lft_incl κ κ'.
   Proof.
     iIntros (??) "_ !> #HE".
diff --git a/theories/rust_typing/tests.v b/theories/rust_typing/tests.v
index f9f69ee3e15dcd9bcfbfa2a7471d7a5151af3afe..27f4eec1de8394ad669295599946ae20874a7020 100644
--- a/theories/rust_typing/tests.v
+++ b/theories/rust_typing/tests.v
@@ -785,13 +785,13 @@ Section test.
   Abort.
 
   Lemma test2 κ κ' :
-    lctx_lft_incl [κ' ⊑ₑ κ'; κ ⊑ₑ κ'] [] κ κ'.
+    lctx_lft_incl [(* κ' ⊑ₑ κ'; *) κ ⊑ₑ κ'] [] κ κ'.
   Proof.
     solve_lft_incl; solve[fail].
   Abort.
 
   Lemma test2' {rt} (T : type rt) κ κ' :
-    lctx_lft_incl (ty_wf_E T ++ [κ' ⊑ₑ κ'; κ ⊑ₑ κ']) [] κ κ'.
+    lctx_lft_incl (ty_wf_E T ++ [(* κ' ⊑ₑ κ';*) κ ⊑ₑ κ']) [] κ κ'.
   Proof.
     solve_lft_incl; solve[fail].
   Abort.
@@ -843,6 +843,15 @@ Section test.
   Proof.
     solve_lft_incl_list; solve[fail].
   Abort.
+
+  (* This demonstrates that we have to expand both external and local lifetimes from the same direction.
+     If we expand local lifetimes left to right and external lifetimes right to left,
+     we may fail to make any progress. *)
+  Lemma test9 κ κ' κ'' c1 :
+    lctx_lft_incl [κ ⊑ₑ κ'] [κ' ⊑ₗ{ c1} [κ'']] κ κ''.
+  Proof.
+    solve_lft_incl; solve[fail].
+  Abort.
 End test.
 
 (** solve_lft_alive *)
@@ -1044,6 +1053,18 @@ Section test.
   Abort.
 End test.
 
+(** optimize_elctx *)
+Section test.
+  Context `{!typeGS Σ}.
+
+  Lemma test1 E1 κ1 κ2 :
+    ∃ K0, K0 ⊆+ (κ1 ⊑ₑ κ2) :: (κ1 ⊑ₑ κ1) :: (κ2 ⊑ₑ κ1) :: E1 ∧ K0 = (κ1 ⊑ₑ κ2) :: (κ2 ⊑ₑ κ1) :: E1.
+  Proof.
+    eexists _. split.
+    { optimize_elctx. }
+    done.
+  Abort.
+End test.
 
 
 (** solve_elctx_sat *)