NotBad4U

require open Stdlib.Prop Stdlib.Set Stdlib.FOL Stdlib.HOL;

constant symbol Lev: TYPE;
constant symbol lsuc: Lev → Lev;

notation lsuc prefix 10;


constant symbol Set₀: Lev;
symbol Set₁ ≔ lsuc Set₀;

NotBad4U

/**********
The standard library use this rewrites rules in Z and Pos that has been prove confluent.

(VAR
  a: Z
  b: Z
  x : P
  q : P
  y : P
)

NotBad4U

// require open test.Z Stdlib.Set Stdlib.Prop;
require open tests.OK.Z tests.OK.Pos tests.OK.Set;

constant symbol R : TYPE;

symbol var : ℤ → ℤ → R;
/* semantics: [var k x] = k * x
note that the second argument could be any type that has a ring structure
(we then would take R : TYPE → TYPE) */
constant symbol cst:ℤ → R;

NotBad4U

require open Stdlib.Nat Stdlib.Z Stdlib.Set Stdlib.Prop Stdlib.Bool Stdlib.Comp Stdlib.List;

constant symbol R : TYPE;

constant symbol cst:ℤ → R;

symbol var : ℤ → ℕ → R;
/* semantics: [var k x] = k * x
note that the second argument could be any type that has a ring structure
(we then would take R : TYPE → TYPE) */

NotBad4U

require open Stdlib.Z Stdlib.Set Stdlib.Prop;

constant symbol R : TYPE;

symbol var : ℤ → ℤ → R;
/* semantics: [var k x] = k * x
note that the second argument could be any type that has a ring structure
(we then would take R : TYPE → TYPE) */
constant symbol cst:ℤ → R;
symbol opp:R → R;

NotBad4U

require open Stdlib.Prop;
require open Stdlib.FOL;
require open Stdlib.HOL;
require open Stdlib.Eq;
require open Stdlib.Set;
require open Stdlib.Z;
require open Stdlib.Pos;
require open Stdlib.Bool;
require open Stdlib.Comp;
require open Stdlib.Impred;

NotBad4U

require open Stdlib.Prop;
require open Stdlib.FOL;
require open Stdlib.Eq;
require open Stdlib.Nat;
require Stdlib.Bool;
require open Stdlib.Set;
require open Stdlib.List;
require open Stdlib.Prod;
require open Stdlib.Tactic;

NotBad4U

require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq Stdlib.Pos Stdlib.Bool;



inductive ℤ : TYPE ≔ // \BbbZ
| Z0 : ℤ
| Zpos : ℙ → ℤ
| Zneg : ℙ → ℤ;

constant symbol int : Set;

NotBad4U

require open Stdlib.FOL;
require open Stdlib.Prop;
require open Stdlib.Set;
require open Stdlib.Nat;
require open Stdlib.Bool;
require open Stdlib.Eq;
require open Stdlib.Z;
require open Stdlib.List;

// References use

NotBad4U

// PRELUDE ##############
// Définitions intuitioniste nécessaires pour illustrer le problème dans Classic.

constant symbol Prop : TYPE;

injective symbol π : Prop → TYPE; // `p

constant symbol ∨ : Prop → Prop → Prop; notation ∨ infix left 6; // \/ or \vee

constant symbol ∨ᵢ₁ [p q] : π p → π (p ∨ q);