genealized zmap_mapi_Proper_equal

rems-project · Nov 25, 2023 · c9cc090 · c9cc090
1 parent 7a7b96d
commit c9cc090
Showing 1 changed file with 7 additions and 4 deletions.
diff --git a/coq/Proofs/ProofsAux.v b/coq/Proofs/ProofsAux.v
@@ -286,19 +286,22 @@ Section ZMapAux.
   (* Simple case *)
   #[global] Instance zmap_mapi_Proper_equal
     {A B : Type}
-    (f : ZMap.key -> A -> B)
   :
-  Proper ((ZMap.Equal) ==> (ZMap.Equal)) (ZMap.mapi f).
+  Proper ((eq ==> eq ==> eq) ==>
+      (ZMap.Equal) ==> (ZMap.Equal)) (@ZMap.mapi A B ).
   Proof.
-    intros a1 a2 H.
+    intros f1 f2 Ef a1 a2 H.
     unfold ZMap.Equal in *.
     intros k.
     specialize (H k).
     rewrite mapi_o.
     rewrite mapi_o.
     -
       unfold option_map.
-      repeat break_match;invc H; reflexivity.
+      repeat break_match;invc H.
+      f_equiv.
+      apply Ef;reflexivity.
+      reflexivity.
     -
       intros x y e HF;rewrite HF;reflexivity.
     -