1 files changed, 2 insertions, 3 deletions

diff --git a/server/formal/period_seq.v b/server/formal/period_seq.v
index 705e505..8433bc6 100644
--- a/server/formal/period_seq.v
+++ b/server/formal/period_seq.v
@@ -13,9 +13,8 @@ Record period_seq :=
 *)
 
 Definition period_seq := list ne_period.
-
-Definition period_seq_nf (ps : period_seq) :=
-  Sorted period_before ps.
+Definition period_seq_nf : period_seq → Prop :=
+  Sorted period_before.
 
 Instance period_seq_elem_of : ElemOf timestamp period_seq :=
   λ t, Exists (λ p, t ∈ p).