diff --git a/_CoqProject b/_CoqProject
index 942d29768a2329b3fc285c2a6aee0f9e92b5dc6a..f28fdc1d19db5711a04b3bd59141da2f694744fb 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -34,6 +34,7 @@ prelude/sets.v
 prelude/decidable.v
 prelude/list.v
 prelude/error.v
+prelude/functions.v
 algebra/option.v
 algebra/cmra.v
 algebra/cmra_big_op.v
diff --git a/prelude/functions.v b/prelude/functions.v
new file mode 100644
index 0000000000000000000000000000000000000000..2e4c93caaab6e18a2fc09df2dc4658ab03c5aa05
--- /dev/null
+++ b/prelude/functions.v
@@ -0,0 +1,31 @@
+From prelude Require Export base tactics.
+
+Section definitions.
+  Context {A T : Type} `{∀ a b : A, Decision (a = b)}.
+  Global Instance fn_insert : Insert A T (A → T) :=
+    λ a t f b, if decide (a = b) then t else f b.
+  Global Instance fn_alter : Alter A T (A → T) :=
+    λ (g : T → T) a f b, if decide (a = b) then g (f a) else f b.
+End definitions.
+
+(* For now, we only have the properties here that do not need a notion
+   of equality of functions. *)
+
+Section functions.
+  Context {A T : Type} `{∀ a b : A, Decision (a = b)}.
+
+  Lemma fn_lookup_insert (f : A → T) a t : <[a:=t]>f a = t.
+  Proof. unfold insert, fn_insert. by destruct (decide (a = a)). Qed.
+  Lemma fn_lookup_insert_rev  (f : A → T) a t1 t2 :
+    <[a:=t1]>f a = t2 → t1 = t2.
+  Proof. rewrite fn_lookup_insert. congruence. Qed.
+  Lemma fn_lookup_insert_ne (f : A → T) a b t : a ≠ b → <[a:=t]>f b = f b.
+  Proof. unfold insert, fn_insert. by destruct (decide (a = b)). Qed.
+
+  Lemma fn_lookup_alter (g : T → T) (f : A → T) a : alter g a f a = g (f a).
+  Proof. unfold alter, fn_alter. by destruct (decide (a = a)). Qed.
+  Lemma fn_lookup_alter_ne (g : T → T) (f : A → T) a b :
+    a ≠ b → alter g a f b = f b.
+  Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
+
+End functions.