Add list_fmap_inj1, Z_to_little_endian_lookup_Some and little_endian_to_Z_spec

Some more lemmas...

theories/list.v

@@ -3757,6 +3757,10 @@ Section fmap.
     intros [|??]; intros; f_equal/=; simplify_eq; auto.
   Qed.
 
+  Lemma list_fmap_inj_1 (f1 f2 : A → B) l x :
+    f1 <$> l = f2 <$> l → x ∈ l → f1 x = f2 x.
+  Proof. intros Hf Hin. induction Hin; naive_solver. Qed.
+
   Definition fmap_nil : f <$> [] = [] := eq_refl.
   Definition fmap_cons x l : f <$> x :: l = f x :: (f <$> l) := eq_refl.