diff --git a/theories/Sets/GCHtoAC.v b/theories/Sets/GCHtoAC.v
index e333a03a2d5..37a1727b5ef 100644
--- a/theories/Sets/GCHtoAC.v
+++ b/theories/Sets/GCHtoAC.v
@@ -8,17 +8,15 @@ From HoTT.Sets Require Import Ordinals Hartogs Powers GCH AC.
 
 Open Scope type.
 
-(* The proof of Sierpinski's results that GCH implies AC given in this file consists of 2 ingredients:
+(* The proof of Sierpinski's results that GCH implies AC given in this file consists of two ingredients:
    1. Adding powers of infinite sets does not increase the cardinality (path_infinite_power).
    2. A variant of Cantor's theorem saying that P(X) <= (X + Y) implies P(X) <= Y for large X (Cantor_injects_injects).
-   Those are used to obtain that cardinality-controlled functions are well-behaved in the presence of GCH (Sierpinski),
-   from which we obtain by instantiation with the Hartogs number that every set embeds into an ordinal,
-   which is enough to conclude GCH -> AC (GCH_AC) since the well-ordering theorem implies AC (WO_AC). *)
+   Those are used to obtain that cardinality-controlled functions are well-behaved in the presence of GCH (Sierpinski), from which we obtain by instantiation with the Hartogs number that every set embeds into an ordinal, which is enough to conclude GCH -> AC (GCH_AC) since the well-ordering theorem implies AC (WO_AC). *)
 
 
 (** * Constructive equivalences *)
 
-(* For the 1. ingredient, we establish a bunch of paths and conclude the wished result by equational reasoning. *)
+(* For the first ingredient, we establish a bunch of paths and conclude the desired result by equational reasoning. *)
 
 Section Preparation.
 
@@ -63,7 +61,6 @@ Proof.
 Qed.
 
 
-
 (** * Equivalences relying on LEM **)
 
 Context {EM : ExcludedMiddle}.
@@ -124,7 +121,6 @@ Proof.
 Qed.
 
 
-
 (** * Equivalences on infinite sets *)
 
 Lemma path_infinite_unit (X : HSet) :
@@ -143,11 +139,9 @@ Proof.
 Qed.
 
 
-
 (** * Variants of Cantors's theorem *)
 
-(* For the 2. ingredient, we give a preliminary version (Cantor_path_inject) to see the idea,
-   as well as a stronger refinement (Cantor_injects_injects) which is then a mere reformulation. *)
+(* For the second ingredient, we give a preliminary version (Cantor_path_inject) to see the idea, as well as a stronger refinement (Cantor_injects_injects) which is then a mere reformulation. *)
 
 Context {PR : PropResizing}.
 
@@ -241,7 +235,6 @@ Qed.
 End Preparation.
 
 
-
 (** * Sierpinski's Theorem *)
 
 Section Sierpinski.
@@ -260,9 +253,7 @@ Hypothesis HN_ninject : forall X, ~ InjectsInto (HN X) X.
 Variable HN_bound : nat.
 Hypothesis HN_inject : forall X, InjectsInto (HN X) (power_iterated X HN_bound).
 
-(* This section then concludes the intermediate result that abstractly,
-   any function HN behaving like the Hartogs number is tamed in the presence of GCH.
-   Morally we show that X <= HN(X) for all X, we just ensure that X is large enough by considering P(N + X). *)
+(* This section then concludes the intermediate result that abstractly, any function HN behaving like the Hartogs number is tamed in the presence of GCH.  Morally we show that X <= HN(X) for all X, we just ensure that X is large enough by considering P(N + X). *)
 
 Lemma InjectsInto_sum X Y X' Y' :
   InjectsInto X X' -> InjectsInto Y Y' -> InjectsInto (X + Y) (X' + Y').
@@ -278,8 +269,7 @@ Proof.
   - apply ap. apply Hg. apply path_sum_inr with X'. apply H.
 Qed.
 
-(* The main proof is by induction on the cardinality bound for HN.
-   As the Hartogs number is bounded by P^3(X), we'd actually just need finitely many instances of GCH. *)
+(* The main proof is by induction on the cardinality bound for HN.  As the Hartogs number is bounded by P^3(X), we'd actually just need finitely many instances of GCH. *)
 
 Lemma Sierpinski_step (X : HSet) n :
   GCH -> infinite X -> powfix X -> InjectsInto (HN X) (power_iterated X n) -> InjectsInto X (HN X).