diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-22 14:39:25 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-22 14:39:25 -0400 |
| commit | f92702c213de142047232c88e0464961614b3c93 (patch) | |
| tree | bb1264d37ea0e15b12a341af6b62f181a9674c64 /src/Util/LetIn.v | |
| parent | f0bf0cec1aa88998fe9af99a0d9ea9311fffa703 (diff) | |
Add more specific form of Proper_Let_In_nd_changebody
Diffstat (limited to 'src/Util/LetIn.v')
| -rw-r--r-- | src/Util/LetIn.v | 4 |
1 files changed, 4 insertions, 0 deletions
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. |