Minor style tweaks

theories/finite.v

@@ -376,8 +376,9 @@ Section sig_finite.
   Lemma list_filter_sig_filter (l : list A) :
     proj1_sig <$> list_filter_sig l = filter P l.
   Proof.
-    induction l as [| a l IH]; cbn; [done |].
-    destruct (decide _); cbn; by rewrite IH.
+    induction l as [| a l IH]; [done |].
+    simpl; rewrite filter_cons.
+    destruct (decide _); csimpl; by rewrite IH.
   Qed.
 
   Context `{Finite A} `{∀ x, ProofIrrel (P x)}.

theories/list.v

@@ -3478,7 +3478,7 @@ Section fmap.
   Proof.
     intros (y, (E, I))%elem_of_list_fmap_2. by rewrite (inj f) in I.
   Qed.
-  Lemma elem_of_list_fmap_inj `{!Inj (=) (=) f} l x : x ∈ l ↔ f x ∈ f <$> l.
+  Lemma elem_of_list_fmap_inj `{!Inj (=) (=) f} l x : f x ∈ f <$> l ↔ x ∈ l.
   Proof.
     naive_solver eauto using elem_of_list_fmap_1, elem_of_list_fmap_2_inj.
   Qed.

theories/proof_irrel.v

@@ -38,7 +38,7 @@ Proof.
   destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
   f_equal. apply proof_irrel.
 Qed.
-Instance proj1_inj_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)} :
+Instance proj1_sig_inj `(P : A → Prop) `{∀ x, ProofIrrel (P x)} :
   Inj (=) (=) (proj1_sig (P:=P)).
 Proof. intros ??. apply (sig_eq_pi P). Qed.
 Lemma exists_proj1_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}