these two have been upstreamed

theories/simplang/base.v

@@ -15,16 +15,6 @@ Definition binder_to_list (b : binder) : list string :=
   | BAnon => []
   end.
 
-Lemma fst_map_zip {A B C} `{!EqDecision A} `{!Countable A} (m1 : gmap A B) (m2 : gmap A C) :
-  (∀ k : A, is_Some (m1 !! k) → is_Some (m2 !! k)) →
-  fst <$> map_zip m1 m2 = m1.
-Proof. move => ?. by apply: map_fmap_zip_with_l. Qed.
-
-Lemma snd_map_zip {A B C} `{!EqDecision A} `{!Countable A} (m1 : gmap A B) (m2 : gmap A C) :
-  (∀ k : A, is_Some (m2 !! k) → is_Some (m1 !! k)) →
-  snd <$> map_zip m1 m2 = m2.
-Proof. move => ?. by apply: map_fmap_zip_with_r. Qed.
-
 Lemma take_lookup_Some {A} n k (l : list A) x:
   take n l !! k = Some x ↔ l !! k = Some x ∧ k < n.
 Proof.