diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index a5947bf6bd73de3696deba1693d6e19b25ab7ddc..40ea3607e6ae1b44ab4e13e89d023b12380828bb 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -33,9 +33,7 @@ Proof.
   rewrite big_sepL_app. iDestruct "Hel" as "[Hvl Hel]".
   iAssert ([∗ list] y ∈ [], Q y)%I with "[Hvl]" as "Hvl".
   { by rewrite big_sepL_nil. }
-  (*assert (length ((of_val <$> ([] : list val)) ++ el) = length el) as Hlen by reflexivity.*)
-  remember [] as vl. clear Heqvl. (*remember (length el) as n. clear Heqn.*)
-  iInduction el as [|e el] "IH" forall (vl).
+  remember [] as vl. clear Heqvl. iInduction el as [|e el] "IH" forall (vl).
   - rewrite app_nil_r. by iApply "HΦ".
   - destruct Hf as [vf Hf]. set (K := AppRCtx vf vl el).
     rewrite (_ : App f ((of_val <$> vl) ++ e :: el) = fill_item K e); last first.