few more uses of ap_pV

Signed-off-by: Ali Caglayan <[email protected]>

Author: Alizter

theories/Homotopy/Smash.v

@@ -181,10 +181,9 @@ Section Smash.
     (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) (a b : X)
     : ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel' a b) = Pgl a @ (Pgl b)^.
   Proof.
-    lhs napply ap_pp.
+    lhs napply ap_pV.
     f_ap.
     1: apply Smash_rec_beta_gluel.
-    lhs napply ap_V.
     apply inverse2.
     apply Smash_rec_beta_gluel.
   Defined.
@@ -193,10 +192,9 @@ Section Smash.
     (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) (a b : Y)
     : ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer' a b) = Pgr a @ (Pgr b)^.
   Proof.
-    lhs napply ap_pp.
+    lhs napply ap_pV.
     f_ap.
     1: apply Smash_rec_beta_gluer.
-    lhs napply ap_V.
     apply inverse2.
     apply Smash_rec_beta_gluer.
   Defined.

theories/Homotopy/Wedge.v

@@ -338,8 +338,7 @@ Proof.
       change (?t = _) with (t = loop_susp_unit X x).
       lhs napply (ap_compose (psusp_pinch X)).
       lhs napply (ap _ (psusp_pinch_beta_merid x)).
-      lhs napply ap_pp.
-      lhs napply (ap (fun x => _ @ x) (ap_V _ _)).
+      lhs napply ap_pV.
       apply moveR_pV.
       rhs napply (whiskerL _ (wedge_rec_beta_wglue _ _)).
       lhs napply ap_pp.
@@ -369,8 +368,7 @@ Proof.
       change (?t = _) with (t = loop_susp_unit X x).
       lhs napply (ap_compose (psusp_pinch X)).
       lhs napply (ap _ (psusp_pinch_beta_merid x)).
-      lhs napply ap_pp.
-      lhs napply (ap (fun x => _ @ x) (ap_V _ _)).
+      lhs napply ap_pV.
       apply moveR_pV.
       rhs napply (whiskerL _ (wedge_rec_beta_wglue _ _)).
       lhs napply ap_pp.