diff --git a/prelude/functions.v b/prelude/functions.v
index 2e4c93caaab6e18a2fc09df2dc4658ab03c5aa05..bc12965f09d24873bf54f2416f132e87843c4946 100644
--- a/prelude/functions.v
+++ b/prelude/functions.v
@@ -29,3 +29,26 @@ Section functions.
   Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
 
 End functions.
+
+(** "Cons-ing" of functions from nat to T *)
+Section fcons.
+  Context {T : Type}.
+
+  Definition fn_cons (t : T) (f: nat → T) : nat → T :=
+    λ n, match n with
+         | O => t
+         | S n => f n
+         end.
+
+  Definition fn_mcons (ts : list T) (f : nat → T) : nat → T :=
+    fold_right fn_cons f ts.
+End fcons.
+
+Infix ".::" := fn_cons (at level 60, right associativity) : C_scope.
+Infix ".++" := fn_mcons (at level 60, right associativity) : C_scope.
+
+Lemma fn_mcons_app {T : Type} (ts1 ts2 : list T) f :
+  (ts1 ++ ts2) .++ f = ts1 .++ (ts2 .++ f).
+Proof.
+  unfold fn_mcons. rewrite fold_right_app. done.
+Qed.