From 4b1fb93975a54c343c6ede50aeed3f2dccc6f14a Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 17 Nov 2016 17:35:21 -0500
Subject: Add HList.mapt_Proper

---
 src/Util/HList.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

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

diff --git a/src/Util/HList.v b/src/Util/HList.v
index cac84ece2..802ab1ed3 100644
--- a/src/Util/HList.v
+++ b/src/Util/HList.v
@@ -117,6 +117,17 @@ Proof.
   destruct n; [ simpl; tauto | apply fold_right_and_True_hlist' ].
 Qed.
 
+Global Instance mapt_Proper {n A F B}
+  : Proper
+      ((forall_relation (fun x => pointwise_relation _ Logic.eq))
+         ==> forall_relation (fun ts => Logic.eq ==> Logic.eq))
+      (@HList.mapt n A F B).
+Proof.
+  unfold forall_relation, pointwise_relation, respectful.
+  repeat intro; subst; destruct n as [|n]; [ reflexivity | ].
+  induction n; simpl in *; congruence.
+Qed.
+
 Module Tuple.
   Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
   : hlist (fun x => f x = x) xs -> Tuple.map f xs = xs.
-- 
cgit v1.2.3