Add HList.mapt_Proper

1 files changed, 11 insertions, 0 deletions

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.