diff --git a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_mut.v b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_mut.v
index dd682e2e62ca5e68586409f6050df45cb55d13ad..407ac34dba6eed354075e286d558a8c6d399b172 100644
--- a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_mut.v
+++ b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_mut.v
@@ -30,22 +30,6 @@ Proof.
   all: print_remaining_goal.
   Unshelve. all: sidecond_solver.
   Unshelve. all: sidecond_hammer.
-  { (* TODO: currently not handled by the solver *)
-    apply Forall_forall.
-    intros κe Hlft.
-    eapply (lctx_lft_alive_incl ϝ); first sidecond_hook.
-    apply lctx_lft_incl_external.
-    apply elem_of_cons; right.
-    apply elem_of_cons; right.
-    apply elem_of_cons; right.
-    apply elem_of_app; right.
-    apply elem_of_app; right.
-    apply elem_of_app; right.
-    apply elem_of_app; left.
-    unfold_opaque @ty_outlives_E.
-    rewrite /lfts_outlives_E.
-    rewrite elem_of_list_fmap.
-    eexists. split; done. }
   Unshelve. all: print_remaining_sidecond.
 Qed.
 End proof.