SetoidRewrite: slight simplification to IsEpic_HasSection

Author: jdchristensen

contrib/SetoidRewrite.v

@@ -139,8 +139,7 @@ Proposition IsEpic_HasSection {A} `{Is1Cat A}
   SectionOf f -> Epic f.
 Proof.
   intros [right_inverse is_section] c g h eq_gf_hf.
-  apply (fmap (cat_precomp _ right_inverse)) in eq_gf_hf;
-    unfold cat_precomp in eq_gf_hf.
+  apply (fun p => cat_prewhisker p right_inverse) in eq_gf_hf.
   rewrite 2 cat_assoc, is_section, 2 cat_idr in eq_gf_hf.
   exact eq_gf_hf.
 Defined.