Refactor proof of list_to_map_snoc

theories/fin_map_dom.v

@@ -156,7 +156,7 @@ Proof.
   intros m1 m2 EQm. apply elem_of_equiv. intros i.
   rewrite !elem_of_dom, EQm. done.
 Qed.
-Lemma dom_list_to_map {A : Type} (l : list (K * A)) :
+Lemma dom_list_to_map {A} (l : list (K * A)) :
   dom D (list_to_map l : M A) ≡ list_to_set l.*1.
 Proof.
   induction l as [|?? IH].
@@ -204,7 +204,7 @@ Section leibniz.
     (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) →
     dom D (map_imap f m) = X.
   Proof. unfold_leibniz; apply dom_imap. Qed.
-  Lemma dom_list_to_map_L {A : Type} (l : list (K * A)) :
+  Lemma dom_list_to_map_L {A} (l : list (K * A)) :
     dom D (list_to_map l : M A) = list_to_set l.*1.
   Proof. unfold_leibniz. apply dom_list_to_map. Qed.
 End leibniz.

theories/fin_maps.v

@@ -836,16 +836,14 @@ Qed.
 Lemma list_to_map_nil {A} : list_to_map [] = (∅ : M A).
 Proof. done. Qed.
 Lemma list_to_map_cons {A} (l : list (K * A)) i x :
-  list_to_map ((i, x) :: l) = <[i:=x]>(list_to_map l : M A).
+  list_to_map ((i, x) :: l) =@{M A} <[i:=x]>(list_to_map l).
 Proof. done. Qed.
 Lemma list_to_map_snoc {A} (l : list (K * A)) i x :
-  i ∉ l.*1 → list_to_map (l ++ [(i, x)]) = <[i:=x]>(list_to_map l : M A).
+  i ∉ l.*1 → list_to_map (l ++ [(i, x)]) =@{M A} <[i:=x]>(list_to_map l).
 Proof.
-  induction l as [|[k y] l IH]; [done|].
-  intros [Hneq Hni]%not_elem_of_cons. simpl.
-  rewrite (IH Hni).
-  rewrite insert_commute; [done|].
-  rewrite comm; [apply Hneq|apply _].
+  induction l as [|[k y] l IH]; [done|]. csimpl.
+  intros [Hneq Hni]%not_elem_of_cons.
+  by rewrite (IH Hni), insert_commute by done.
 Qed.
 Lemma list_to_map_fmap {A B} (f : A → B) l :
   list_to_map (prod_map id f <$> l) = f <$> (list_to_map l : M A).