diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 3be29dd99e0b87f5723fd5df46aab947c141197a..675899ed9c01d0563b13b56de4049a202821af8c 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -56,7 +56,16 @@ Class lftPreG Σ := LftPreG {
   lft_preG_inh_inG :> inG Σ (authR inhUR);
 }.
 
-(* TODO: Write a Σ for lftPreG *)
+Definition lftΣ : gFunctors :=
+  #[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
+     GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
+Instance subG_stsΣ Σ :
+  subG lftΣ Σ → lftPreG Σ.
+Proof.
+  intros [? [?%subG_inG [?%subG_inG [?%subG_inG [?%subG_inG
+             ?%subG_inG]%subG_inv]%subG_inv]%subG_inv]%subG_inv]%subG_inv.
+  split; first apply _; done.
+Qed.
 
 Module Type lifetime_sig.
   (** Definitions *)