diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 4eabe756de..3281b94a9e 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -930,7 +930,7 @@ Definition grp_prod_corec_natural {X Y A B : Group}
 
 (** The left factor injects into the direct product. *)
 Definition grp_prod_inl {H K : Group}
-  : H $-> (grp_prod H K)
+  : H $-> grp_prod H K
   := grp_prod_corec grp_homo_id grp_homo_const.
 
 (** The left injection is an embedding. *)
@@ -944,7 +944,7 @@ Defined.
 
 (** The right factor injects into the direct product. *)
 Definition grp_prod_inr {H K : Group}
-  : K $-> (grp_prod H K)
+  : K $-> grp_prod H K
   := grp_prod_corec grp_homo_const grp_homo_id.
 
 (** The right injection is an embedding. *)
@@ -995,7 +995,7 @@ Defined.
 
 (** Pairs in direct products can be decomposed *)
 Definition grp_prod_decompose {G H : Group} (g : G) (h : H)
-  : (g, h) = ((g, group_unit) : grp_prod G H) * (group_unit, h).
+  : (g, h) = ((g, 1) : grp_prod G H) * (1, h).
 Proof.
   snrapply path_prod; symmetry.
   - snrapply grp_unit_r.
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
index 21ea46dd7e..4aebf2f80b 100644
--- a/theories/Algebra/Groups/QuotientGroup.v
+++ b/theories/Algebra/Groups/QuotientGroup.v
@@ -253,9 +253,8 @@ Section FirstIso.
     snrapply isequiv_surj_emb.
     1: srapply cancelR_conn_map.
     srapply isembedding_isinj_hset.
-    refine (Quotient_ind_hprop _ _ _); intro x.
-    refine (Quotient_ind_hprop _ _ _); intro y.
-    intros h; simpl in h.
+    srapply Quotient_ind2_hprop.
+    intros x y h; simpl in h.
     apply qglue; cbn.
     apply (equiv_path_sigma_hprop _ _)^-1%equiv in h; cbn in h.
     cbn. rewrite grp_homo_op, grp_homo_inv, h.