Better writing of nodupAx

runtimeverification · Jan 16, 2025 · 4f8646e · 4f8646e
1 parent 9cffbc7
commit 4f8646e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean
@@ -78,7 +78,7 @@ axiom valuesAx     : mapCAx → List V
 axiom sizeAx       : mapCAx → Nat
 axiom includesAx   : mapCAx → mapCAx → Bool -- map inclusion
 axiom choiceAx     : mapCAx → K -- arbitrary key from a map
-axiom nodupAx      : forall al                              : mapCAx, List.Nodup (keysAx K al)
+axiom nodupAx      : forall m, List.Nodup (keysAx K m)
 
 -- Uninterpreted Map implementation
 noncomputable def mapImpl (K V : Type) : MapHookSig K V :=