Switch to strict bulleting everywhere

Solve #82 (closed).

The flag isn't enforced anywhere, but with this we can add it seamlessly (ideally soon after so there aren't more violations that creep in).

theories/fin_maps.v

@@ -451,9 +451,7 @@ Proof. rewrite <-(partial_alter_self ∅) at 2. by rewrite lookup_empty. Qed.
 Lemma delete_commute {A} (m : M A) i j :
   delete i (delete j m) = delete j (delete i m).
 Proof.
-  destruct (decide (i = j)).
-  - by subst.
-  - by apply partial_alter_commute.
+  destruct (decide (i = j)) as [->|]; [done]. by apply partial_alter_commute.
 Qed.
 Lemma delete_insert_ne {A} (m : M A) i j x :
   i ≠ j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
@@ -880,8 +878,7 @@ Lemma map_to_list_empty_inv {A} (m : M A) : map_to_list m = [] → m = ∅.
 Proof. intros Hm. apply map_to_list_empty_inv_alt. by rewrite Hm. Qed.
 Lemma map_to_list_empty' {A} (m : M A) : map_to_list m = [] ↔ m = ∅.
 Proof.
-  split; [apply map_to_list_empty_inv|].
-  - intros ->. apply map_to_list_empty.
+  split; [apply map_to_list_empty_inv|]. intros ->. apply map_to_list_empty.
 Qed.
 
 Lemma map_to_list_insert_inv {A} (m : M A) l i x :