two adaptations to ArToSig now being defined through foldr1_map

UniMath · Jun 11, 2024 · 9ace96a · 9ace96a
1 parent fb7ffc2
commit 9ace96a
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/Modules/Signatures/BindingSig.v b/Modules/Signatures/BindingSig.v
@@ -202,8 +202,7 @@ Section EpiSignatureSig.
       + intros n ar HI m epi_ar.
         intros M N f epif.
         unfold ArToSig,  Arity_to_Signature.
-        rewrite 2!map_cons.
-        rewrite foldr1_cons.
+        rewrite foldr1_map_cons.
         apply isEpi_binProdSig.
         * apply precompEpiFunc.
         * exact epi_ar.
@@ -224,8 +223,7 @@ Section EpiSignatureSig.
       + intros n ar HI m epi_ar.
         intros R epiR.
         unfold ArToSig,  Arity_to_Signature.
-        rewrite 2!map_cons.
-        rewrite foldr1_cons.
+        rewrite foldr1_map_cons.
         apply preserveEpi_binProdFunc.
         * apply productEpisSET.
         * apply precompEpiEpiFunc.