Update Prime.v

Author: tabareau

Prime.v

@@ -2,30 +2,20 @@
 Require Import Relations.
 
 Set Primitive Projections.
-Record sigmaP {A : SProp} {B : A -> SProp} : SProp := sigmaPI { prP1 : A; prP2 : B prP1 }.
-
-Arguments sigmaP A B : clear implicits.
-Arguments sigmaPI {A} B prP1 prP2.
-
-Notation "{ x : A & P }" := (sigmaP A (fun x => P)) : type_scope.
-Notation "x .1" := (prP1 x) (at level 3).
-Notation "x .2" := (prP2 x) (at level 3).
-Notation " ( x ; p ) " := (sigmaPI _ x p).
-
-Inductive sFalse : SProp := .
-Inductive sTrue : SProp := I : sTrue.
 
 From Equations Require Import Equations.
 
+Notation "{ x : A & P }" := (sigmaSP A (fun x => P)) : type_scope.
+Notation "x .1" := (prSP1 x) (at level 3).
+Notation "x .2" := (prSP2 x) (at level 3).
+Notation " ( x ; p ) " := (sigmaSPI _ x p).
+
 (** INTERNAL: Equations binding *)
 (** This binds constants to use by Equations, only the sort, true and
     false propositions are used by the Derive Invert command. Work is in
     progress to use a general registration command as for sigma types below. *)
 
-Equations Logic
-          SProp Id Id_rect Id_rect_r Id_rect_dep_r
-          sFalse sTrue I prod pair
-          relation clos_trans WellFounded well_founded.
+Require Import Equations.ConstantsSProp.  
 
 Register sigmaP as equations.sigmasP.type.
 Register sigmaPI as equations.sigmasP.intro.
@@ -61,7 +51,7 @@ Infix "<=" := invert_le.
 
 Infix "<" := (fun n m => S n <= m).
 
-Definition le_0 : forall n, 0 <= n := fun n => I.
+Definition le_0 : forall n, 0 <= n := fun n => sI.
 
 Definition le_S : forall {m n}, m <= n -> S m <= S n := fun n m e => e.
 
@@ -113,7 +103,7 @@ Check eq_refl : invert_Divide =
 
 Infix "|" := invert_Divide (at level 80). 
 
-Definition divide_0 n : n | 0 := I. 
+Definition divide_0 n : n | 0 := sI. 
 
 Definition divide_S n m (e: S n <= S m) (H: S n | S m - S n) : S n | S m
   := (e;H). 
@@ -168,7 +158,7 @@ Inductive prime (p:nat) : SProp :=
     1 < p -> (forall n, (1 <= n) -> (n < p) -> rel_prime n p) -> prime p.
 
 Goal prime 13.
-  cbn. econstructor. exact I. intro n. 
+  cbn. econstructor. exact sI. intro n. 
   destruct n. inversion 1. intros _ e. cbn in e.
   repeat (try solve [firstorder];
       destruct n; [ cbn;  repeat econstructor; repeat (destruct x; firstorder) |]).