diff --git a/proofs/eo/cpc/programs/Utils.eo b/proofs/eo/cpc/programs/Utils.eo
index b2e1e5ccab2..4997dbc3a97 100644
--- a/proofs/eo/cpc/programs/Utils.eo
+++ b/proofs/eo/cpc/programs/Utils.eo
@@ -91,7 +91,7 @@
 ; - x S: The term to inspect.
 ; return: the head of x, where x is expected to be a function application.
 (define $head ((S Type :implicit) (x S))
-  (eo::match ((T Type) (f (-> T T T)) (x1 T) (x2 T :list))
+  (eo::match ((T Type) (f (-> T U U)) (x1 T) (x2 U :list))
     x
     (((f x1 x2) x1)))
 )