diff --git a/theories/list.v b/theories/list.v
index 1853423ce82d23d1d553ed82a258c5a539ee9e37..2df51d67df614d647d7f7146df592de3ca008683 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2283,7 +2283,8 @@ Section Forall2.
   Proof.
     intro. unfold sublist_lookup, sublist_alter.
     erewrite <-Forall2_length by eauto; intros; simplify_option_equality.
-    apply Forall2_app_l; rewrite ?take_length_le by lia; auto using Forall2_take.
+    apply Forall2_app_l;
+      rewrite ?take_length_le by lia; auto using Forall2_take.
     apply Forall2_app_l; erewrite Forall2_length, take_length,
       drop_length, <-Forall2_length, Min.min_l by eauto with lia; [done|].
     rewrite drop_drop; auto using Forall2_drop.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index b1af8fdcb54d10aa145326a60dab55351577b879..b6b6af9a5f177a910abc59af767b3d0bdcb649f7 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -48,12 +48,7 @@ Qed.
 
 Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
 Global Instance: FinCollection A C.
-Proof.
-  split.
-  * apply _.
-  * done.
-  * by intros [??].
-Qed.
+Proof. split. apply _. done. by intros [??]. Qed.
 Global Instance: CollectionOps A C.
 Proof.
   split.
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index 77b7c2c485d79bcc7f3097a1e2454e34de1d77e8..12e2491a6ed23386c8ae1aaa263c3431a15bf9c3 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -9,24 +9,20 @@ Instance: ProofIrrel True.
 Proof. by intros [] []. Qed.
 Instance: ProofIrrel False.
 Proof. by intros []. Qed.
-
 Instance and_pi (A B : Prop) :
   ProofIrrel A → ProofIrrel B → ProofIrrel (A ∧ B).
 Proof. intros ?? [??] [??]. by f_equal. Qed.
 Instance prod_pi (A B : Type) :
   ProofIrrel A → ProofIrrel B → ProofIrrel (A * B).
 Proof. intros ?? [??] [??]. by f_equal. Qed.
-
 Instance eq_pi {A} `{∀ x y : A, Decision (x = y)} (x y : A) :
   ProofIrrel (x = y).
 Proof.
   intros ??. apply eq_proofs_unicity.
   intros x' y'. destruct (decide (x' = y')); tauto.
 Qed.
-
 Instance Is_true_pi (b : bool) : ProofIrrel (Is_true b).
 Proof. destruct b; simpl; apply _. Qed.
-
 Lemma sig_eq_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   (x y : sig P) : x = y ↔ `x = `y.
 Proof.
@@ -34,7 +30,6 @@ Proof.
   destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
   f_equal. apply proof_irrel.
 Qed.
-
 Lemma exists_proj1_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   (x : sig P) p : `x ↾ p = x.
 Proof. by apply (sig_eq_pi _). Qed.