diff --git a/theories/functions.v b/theories/functions.v
index 47349cc0b57cf89eb9facae2296e9c5d704eceb3..af040172bd7f1ceb12b2cc5d3e71b7a5240e3fe4 100644
--- a/theories/functions.v
+++ b/theories/functions.v
@@ -31,23 +31,19 @@ Section functions.
 End functions.
 
 (** "Cons-ing" of functions from nat to T *)
-Section fcons.
-  Context {T : Type}.
+Polymorphic Definition fn_cons {T : Type} (t : T) (f: nat → T) : nat → T :=
+  λ n, match n with
+       | O => t
+       | S n => f n
+       end.
 
-  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 :=
+Polymorphic Definition fn_mcons {T : Type} (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 :
+Polymorphic 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.