diff --git a/theories/algebra/Perms.ec b/theories/algebra/Perms.ec
index 1ebc0e1d7..8e2b65d18 100644
--- a/theories/algebra/Perms.ec
+++ b/theories/algebra/Perms.ec
@@ -3,11 +3,22 @@ require import AllCore List IntDiv Binomial Ring StdOrder.
 (*---*) import IntID IntOrder.
 
 (* -------------------------------------------------------------------- *)
-op allperms_r (n : unit list) (s : 'a list) : 'a list list =
-with n = [] => [[]]
-with n = x::n => flatten (
-    map (fun x => map ((::) x) (allperms_r n (rem x s))) (undup s)).
+op [smt_opaque] allperms_r (n : unit list) (s : 'a list) : 'a list list =
+  with n = [] =>
+    [[]]
+  with n = _ :: n =>
+    flatten (map (fun x => map ((::) x) (allperms_r n (rem x s))) (undup s)).
 
+lemma allperms_r0 (s : 'a list) :
+  allperms_r [] s = [[]]
+by done. 
+
+lemma allperms_rS (x : unit) (n : unit list) (s : 'a list) :
+  allperms_r (x :: n) s = flatten (
+    map (fun x => map ((::) x) (allperms_r n (rem x s))) (undup s))
+by done.
+
+(* -------------------------------------------------------------------- *)
 op allperms (s : 'a list) = allperms_r (nseq (size s) tt) s.
 
 (* -------------------------------------------------------------------- *)