diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2f1a7afd80b9058e60da7df275227abc5a6dcda2..b85be1f3867f13ddcc760d33fc7f1bf66d09452c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -96,6 +96,19 @@ Section finmap.
   Proof. intros Hm ?. subst. rewrite lookup_delete in Hm. now apply None_not_is_Some in Hm. Qed.
   Lemma lookup_delete_ne (m : M A) i j : i ≠ j → delete i m !! j = m !! j.
   Proof. apply lookup_partial_alter_ne. Qed.
+  Lemma lookup_delete_None (m : M A) i j : m !! j = None → delete i m !! j = None.
+  Proof.
+    destruct (decide (i = j)).
+     subst. now rewrite lookup_delete.
+    now rewrite lookup_delete_ne.
+  Qed.
+  Lemma delete_lookup_None (m : M A) i : m !! i = None → delete i m = m.
+  Proof.
+    intros. apply finmap_eq. intros j. destruct (decide (i = j)).
+     subst. rewrite lookup_delete. congruence.
+    now apply lookup_delete_ne.
+  Qed.
+
   Lemma delete_empty i : delete i (∅ : M A) = ∅.
   Proof. rewrite <-(partial_alter_self ∅) at 2. now rewrite lookup_empty. Qed.
   Lemma delete_singleton i (x : A) : delete i {{ (i, x) }} = ∅.
diff --git a/theories/trs.v b/theories/trs.v
index 5a6d6db45c3af18df219d7a5432fa75013d60688..efb65063e758cb19b28d48f18418f1ac1db5dc83 100644
--- a/theories/trs.v
+++ b/theories/trs.v
@@ -90,8 +90,10 @@ Hint Resolve rtc_once rtc_r tc_r : trs.
 Section subrel.
   Context {A} (R1 R2 : relation A) (Hsub : subrelation R1 R2).
 
+  Lemma red_subrel x : red R1 x → red R2 x.
+  Proof. intros [y ?]. exists y. now apply Hsub. Qed.
   Lemma nf_subrel x : nf R2 x → nf R1 x.
-  Proof. intros Hnf [y ?]. destruct Hnf. exists y. now apply Hsub. Qed.
+  Proof. intros H1 H2. destruct H1. now apply red_subrel. Qed.
 
   Global Instance rtc_subrel: subrelation (rtc R1) (rtc R2).
   Proof.