From f92702c213de142047232c88e0464961614b3c93 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 22 Oct 2016 14:39:25 -0400
Subject: Add more specific form of Proper_Let_In_nd_changebody

---
 src/Util/LetIn.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/Util/LetIn.v')

diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v
index db09baf9c..12e1e6d43 100644
--- a/src/Util/LetIn.v
+++ b/src/Util/LetIn.v
@@ -20,6 +20,10 @@ Global Instance Proper_Let_In_nd_changevalue {A B} (RA:relation A) {RB:relation
   : Proper (RA ==> (RA ==> RB) ==> RB) (Let_In (P:=fun _=>B)).
 Proof. cbv; intuition. Qed.
 
+Lemma Proper_Let_In_nd_changebody_eq {A P R} {Reflexive_R:@Reflexive P R} {x}
+  : Proper ((fun f g => forall a, x = a -> R (f a) (g a)) ==> R) (@Let_In A (fun _ => P) x).
+Proof. lazy; intros; subst; auto; congruence. Qed.
+
 Definition app_Let_In_nd {A B T} (f:B->T) (e:A) (C:A->B)
   : f (Let_In e C) = Let_In e (fun v => f (C v)) := eq_refl.
 
-- 
cgit v1.2.3