diff --git a/transfer/examples/reflexive/reflexive.tra b/transfer/examples/reflexive/reflexive.tra
index 9f8533f7a..8d28f0db0 100644
--- a/transfer/examples/reflexive/reflexive.tra
+++ b/transfer/examples/reflexive/reflexive.tra
@@ -29,3 +29,12 @@ reflexivize _ t = composOp ? ? compos_Tree ? reflexivize t
 
 reflexivize_S : Tree S -> Tree S
 reflexivize_S = reflexivize S
+
+{-
+With a type checker and hidden arguments we could write:
+
+reflexivize : {C : Cat} -> Tree C -> Tree C
+reflexivize (PredV2 v s o) | s == o = ReflV2 v s
+reflexivize t = composOp reflexivize t
+
+-}
\ No newline at end of file