diff --git a/Comp.lp b/Comp.lp
index 65f717d..f6c8898 100644
--- a/Comp.lp
+++ b/Comp.lp
@@ -49,17 +49,17 @@ with isGe Gt ↪ true;
 
 // Discriminate constructors
 
-symbol Lt≠Eq : π (Lt ≠ Eq) ≔
+opaque symbol Lt≠Eq : π (Lt ≠ Eq) ≔
 begin
   assume h; refine ind_eq h (λ n, istrue(isEq n)) ⊤ᵢ
 end;
 
-symbol Gt≠Eq : π (Gt ≠ Eq) ≔
+opaque symbol Gt≠Eq : π (Gt ≠ Eq) ≔
 begin
   assume h; refine ind_eq h (λ n, istrue(isEq n)) ⊤ᵢ
 end;
 
-symbol Gt≠Lt : π (Gt ≠ Lt) ≔
+opaque symbol Gt≠Lt : π (Gt ≠ Lt) ≔
 begin
   assume h; refine ind_eq h (λ n, istrue(isLt n)) ⊤ᵢ
 end;
@@ -72,7 +72,7 @@ rule opp Eq ↪ Eq
 with opp Lt ↪ Gt
 with opp Gt ↪ Lt;
 
-symbol opp_idem c : π (opp (opp c) = c) ≔
+opaque symbol opp_idem c : π (opp (opp c) = c) ≔
 begin
   induction { reflexivity; } { reflexivity; } { reflexivity; }
 end;
diff --git a/Pos.lp b/Pos.lp
index e4014ed..55fa402 100644
--- a/Pos.lp
+++ b/Pos.lp
@@ -37,22 +37,22 @@ with isH H     ↪ true;
 
 // Discriminate constructors
 
-symbol I≠H [x] : π (I x ≠ H) ≔
+opaque symbol I≠H [x] : π (I x ≠ H) ≔
 begin
   assume x h; refine ind_eq h (λ x, istrue(isH x)) ⊤ᵢ;
 end;
 
-symbol O≠H [x] : π (O x ≠ H) ≔
+opaque symbol O≠H [x] : π (O x ≠ H) ≔
 begin
   assume x h; refine ind_eq h (λ x, istrue(isH x)) ⊤ᵢ;
 end;
 
-symbol I≠O [x y] : π (I x ≠ O y) ≔
+opaque symbol I≠O [x y] : π (I x ≠ O y) ≔
 begin
   assume x y h; refine ind_eq h (λ x, istrue(isO x)) ⊤ᵢ;
 end;
 
-opaque symbol caseH x : π(x = H ∨ x ≠ H) ≔
+opaque opaque symbol caseH x : π(x = H ∨ x ≠ H) ≔
 begin
   induction
   { assume x h; apply ∨ᵢ₂; refine I≠H }
@@ -68,7 +68,7 @@ rule projO (O $x) ↪ $x
 with projO (I $x) ↪ I $x
 with projO H ↪ H;
 
-opaque symbol O_inj p q : π(O p = O q) → π(p = q) ≔
+opaque opaque symbol O_inj p q : π(O p = O q) → π(p = q) ≔
 begin
   assume p q h; apply feq projO h
 end;
@@ -79,7 +79,7 @@ rule projI (I $x) ↪ $x
 with projI (O $x) ↪ O $x
 with projI H ↪ H;
 
-opaque symbol I_inj p q : π(I p = I q) → π(p = q) ≔
+opaque opaque symbol I_inj p q : π(I p = I q) → π(p = q) ≔
 begin
   assume p q h; apply feq projI h
 end;
@@ -102,7 +102,7 @@ with val (I $x) ↪ val (O $x) +1;
 
 assert ⊢ val (O (I H)) ≡ 6;
 
-opaque symbol valS x : π(val (succ x) = val x +1) ≔
+opaque opaque symbol valS x : π(val (succ x) = val x +1) ≔
 begin
   induction
   { assume x h; simplify; rewrite h; reflexivity }
@@ -110,7 +110,7 @@ begin
   { reflexivity }
 end;
 
-opaque symbol val_surj [n] : π(n ≠ 0 ⇒ `∃ x, val x = n) ≔
+opaque opaque symbol val_surj [n] : π(n ≠ 0 ⇒ `∃ x, val x = n) ≔
 begin
   induction
   { assume h; apply ⊥ₑ; apply h; reflexivity }
@@ -121,7 +121,7 @@ begin
   }
 end;
 
-opaque symbol val≠0 x : π(val x ≠ 0) ≔
+opaque opaque symbol val≠0 x : π(val x ≠ 0) ≔
 begin
   induction
   { assume x h; refine s≠0 }
@@ -131,12 +131,12 @@ begin
   { refine s≠0 }
 end;
 
-opaque symbol 2*val≠0 x : π(val x + val x ≠ 0) ≔
+opaque opaque symbol 2*val≠0 x : π(val x + val x ≠ 0) ≔
 begin
   assume x h; apply ⊥ₑ; apply val≠0 x; apply 2*=0; apply h
 end;
 
-opaque symbol val_inj [x y] : π(val x = val y) → π(x = y) ≔
+opaque opaque symbol val_inj [x y] : π(val x = val y) → π(x = y) ≔
 begin
   induction
   { assume x h; induction
@@ -163,7 +163,7 @@ end;
 
 // ℕ-like Induction Principle
 
-symbol ind_ℙeano p : π (p H) → (Π x, π (p x) → π (p (succ x))) → Π x, π (p x) ≔
+opaque symbol ind_ℙeano p : π (p H) → (Π x, π (p x) → π (p (succ x))) → Π x, π (p x) ≔
 begin
   assume p pH psucc;
   have i: π(`∀ n, `∀ x, val x = n ⇒ p x) {
@@ -216,7 +216,7 @@ assert ⊢ add (O (I (O (I (O (I (O (I H))))))))
 
 // Interaction of succ and add
 
-symbol succ_add x y : π (succ (add x y) = add_carry x y) ≔
+opaque symbol succ_add x y : π (succ (add x y) = add_carry x y) ≔
 begin
   induction
   // case I
@@ -235,7 +235,7 @@ begin
   { induction { reflexivity } { reflexivity } { reflexivity }  }
 end;
 
-symbol add_succ x y : π (add (succ x) y = succ (add x y)) ≔
+opaque symbol add_succ x y : π (add (succ x) y = succ (add x y)) ≔
 begin
   induction
   // case I
@@ -254,7 +254,7 @@ begin
   { induction { reflexivity } { reflexivity } { reflexivity } }
 end;
 
-symbol add_succ_right x y : π (add x (succ y) = succ (add x y)) ≔
+opaque symbol add_succ_right x y : π (add x (succ y) = succ (add x y)) ≔
 begin
   refine ind_ℙeano (λ x, `∀ y, add x (succ y) = succ (add x y)) _ _
   // case H
@@ -266,7 +266,7 @@ end;
 
 // Associativity of the addition
 
-symbol add_assoc x y z : π (add (add x y) z = add x (add y z)) ≔
+opaque symbol add_assoc x y z : π (add (add x y) z = add x (add y z)) ≔
 begin
   refine ind_ℙeano (λ x, `∀ y, `∀ z, add (add x y) z = add x (add y z)) _ _
   // case H
@@ -279,7 +279,7 @@ end;
 
 // Commutativity of the addition
 
-symbol add_com x y : π (add x y = add y x) ≔
+opaque symbol add_com x y : π (add x y = add y x) ≔
 begin
   refine ind_ℙeano (λ x, `∀ y, add x y = add y x) _ _
   // case H
@@ -297,7 +297,7 @@ rule pos_pred_double (I $x) ↪ I (O $x)
 with pos_pred_double (O $x) ↪ I (pos_pred_double $x)
 with pos_pred_double H      ↪ H;
 
-symbol pos_pred_double_succ x : π (pos_pred_double (succ x) = I x) ≔
+opaque symbol pos_pred_double_succ x : π (pos_pred_double (succ x) = I x) ≔
 begin
   induction
   { assume x xrec; simplify; rewrite xrec; reflexivity }
@@ -305,7 +305,7 @@ begin
   { reflexivity }
 end;
 
-symbol succ_pos_pred_double x : π (succ (pos_pred_double x) = O x) ≔
+opaque symbol succ_pos_pred_double x : π (succ (pos_pred_double x) = O x) ≔
 begin
   induction
    { reflexivity }
@@ -331,7 +331,7 @@ symbol compare x y ≔ compare_acc x Eq y;
 
 // Commutative property of compare
 
-symbol compare_acc_com x y c :
+opaque symbol compare_acc_com x y c :
   π (compare_acc y c x = opp (compare_acc x (opp c) y)) ≔
 begin
   induction
@@ -354,14 +354,14 @@ begin
      { assume c; simplify; rewrite opp_idem; reflexivity } }
 end;
 
-symbol compare_com x y : π (compare y x = opp (compare x y)) ≔
+opaque symbol compare_com x y : π (compare y x = opp (compare x y)) ≔
 begin
   assume x y; refine compare_acc_com x y Eq;
 end;
 
 // Compare decides the equality
 
-symbol compare_acc_nEq x y c : π (c ≠ Eq ⇒ compare_acc x c y ≠ Eq) ≔
+opaque symbol compare_acc_nEq x y c : π (c ≠ Eq ⇒ compare_acc x c y ≠ Eq) ≔
 begin
   induction
   // case I
@@ -383,7 +383,7 @@ begin
      { assume c Hc; refine Hc } }
 end;
 
-symbol compare_decides x y : π (compare x y = Eq ⇒ x = y) ≔
+opaque symbol compare_decides x y : π (compare x y = Eq ⇒ x = y) ≔
 begin
   induction
   // case I
@@ -407,7 +407,7 @@ end;
 
 // Compare with Gt or Lt
 
-symbol compare_Lt x y :
+opaque symbol compare_Lt x y :
   π (compare_acc x Lt y = case_Comp (compare x y) Lt Lt Gt) ≔
 begin
   induction
@@ -438,7 +438,7 @@ begin
   { induction { reflexivity } { reflexivity } { reflexivity } }
 end;
 
-symbol compare_Gt x y :
+opaque symbol compare_Gt x y :
   π (compare_acc x Gt y = case_Comp (compare x y) Gt Lt Gt) ≔
 begin
   induction
@@ -470,27 +470,27 @@ end;
 
 // Compatibility of compare with the addition
 
-symbol compare_H_Lt y : π (compare_acc H Lt y = Lt) ≔
+opaque symbol compare_H_Lt y : π (compare_acc H Lt y = Lt) ≔
 begin
   induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
-symbol compare_Gt_H x : π (compare_acc x Gt H = Gt) ≔
+opaque symbol compare_Gt_H x : π (compare_acc x Gt H = Gt) ≔
 begin
   induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
-symbol compare_H_succ y c : π (compare_acc H c (succ y) = Lt) ≔
+opaque symbol compare_H_succ y c : π (compare_acc H c (succ y) = Lt) ≔
 begin
   induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
-symbol compare_succ_H x c : π (compare_acc (succ x) c H = Gt) ≔
+opaque symbol compare_succ_H x c : π (compare_acc (succ x) c H = Gt) ≔
 begin
   induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
-symbol compare_succ_Lt x y :
+opaque symbol compare_succ_Lt x y :
   π (compare_acc (succ x) Lt y = compare_acc x Gt y) ≔
 begin
   induction
@@ -510,7 +510,7 @@ begin
      { reflexivity } }
 end;
 
-symbol compare_Gt_succ x y :
+opaque symbol compare_Gt_succ x y :
   π (compare_acc x Gt (succ y) = compare_acc x Lt y) ≔
 begin
   assume x y;
@@ -518,7 +518,7 @@ begin
   simplify; rewrite compare_succ_Lt; reflexivity;
 end;
 
-symbol compare_succ_succ x y c :
+opaque symbol compare_succ_succ x y c :
   π (compare_acc (succ x) c (succ y) = compare_acc x c y) ≔
 begin
   induction
@@ -541,7 +541,7 @@ begin
      { reflexivity } }
 end;
 
-symbol compare_compat_add a x y :
+opaque symbol compare_compat_add a x y :
   π (compare (add x a) (add y a) = compare x y) ≔
 begin
   refine ind_ℙeano (λ a, `∀ x, `∀ y, compare (add x a) (add y a) = compare x y) _ _
diff --git a/Z.lp b/Z.lp
index 637a93d..74cf688 100644
--- a/Z.lp
+++ b/Z.lp
@@ -37,17 +37,17 @@ with isZneg (Zneg _) ↪ true;
 
 // Discriminate constructors
 
-symbol Zpos≠Z0 p : π (Zpos p ≠ Z0) ≔
+opaque symbol Zpos≠Z0 p : π (Zpos p ≠ Z0) ≔
 begin
   assume n h; refine ind_eq h (λ n, istrue(isZ0 n)) ⊤ᵢ
 end;
 
-symbol Zneg≠Z0 p : π (Zneg p ≠ Z0) ≔
+opaque symbol Zneg≠Z0 p : π (Zneg p ≠ Z0) ≔
 begin
   assume n h; refine ind_eq h (λ n, istrue(isZ0 n)) ⊤ᵢ
 end;
 
-symbol Zpos≠Zneg p q : π (Zpos p ≠ Zneg q) ≔
+opaque symbol Zpos≠Zneg p q : π (Zpos p ≠ Zneg q) ≔
 begin
   assume x y h; refine ind_eq h (λ n, istrue(isZneg n)) ⊤ᵢ
 end;
@@ -88,17 +88,17 @@ with pred_double (Zneg $p) ↪ Zneg (I $p);
 
 // Interaction of opp and doubling functions
 
-symbol double_opp z : π (double (— z) = — double z) ≔
+opaque symbol double_opp z : π (double (— z) = — double z) ≔
 begin
   induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
-symbol succ_double_opp z : π (succ_double (— z) = — pred_double z) ≔
+opaque symbol succ_double_opp z : π (succ_double (— z) = — pred_double z) ≔
 begin
   induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
-symbol pred_double_opp z : π (pred_double (— z) = — succ_double z) ≔
+opaque symbol pred_double_opp z : π (pred_double (— z) = — succ_double z) ≔
 begin
   induction { reflexivity } { reflexivity } { reflexivity }
 end;
@@ -117,7 +117,7 @@ with sub H      (I $q) ↪ Zneg (O $q)
 with sub H      (O $q) ↪ Zneg (pos_pred_double $q)
 with sub H       H     ↪ Z0;
 
-symbol sub_same z : π (sub z z = Z0) ≔
+opaque symbol sub_same z : π (sub z z = Z0) ≔
 begin
   induction
    { assume x xrec; simplify; rewrite xrec; reflexivity }
@@ -125,7 +125,7 @@ begin
    { reflexivity }
 end;
 
-symbol sub_opp x y : π (— sub x y = sub y x) ≔
+opaque symbol sub_opp x y : π (— sub x y = sub y x) ≔
 begin
   induction
   // case I
@@ -158,7 +158,7 @@ with Zneg $x + Zneg $y ↪ Zneg (add $x $y);
 
 // Interaction of addition with opposite
 
-symbol distr_—_+ x y : π (— (x + y) = — x + — y) ≔
+opaque symbol distr_—_+ x y : π (— (x + y) = — x + — y) ≔
 begin
   induction
   // case Z0
@@ -179,7 +179,7 @@ end;
 
 // Commutativity of addition
 
-symbol +_com x y : π (x + y = y + x) ≔
+opaque symbol +_com x y : π (x + y = y + x) ≔
 begin
   induction
   // case Z0
@@ -200,7 +200,7 @@ end;
 
 // Interaction of succ and doubling functions
 
-symbol pred_double_succ x : π (pred_double (x + Zpos H) = succ_double x) ≔
+opaque symbol pred_double_succ x : π (pred_double (x + Zpos H) = succ_double x) ≔
 begin
   induction
    { reflexivity }
@@ -208,7 +208,7 @@ begin
    { induction { reflexivity } { reflexivity } { reflexivity } }
 end;
 
-symbol succ_pred_double x : π (pred_double x + Zpos H = double x) ≔
+opaque symbol succ_pred_double x : π (pred_double x + Zpos H = double x) ≔
 begin
   induction
    { reflexivity }
@@ -216,12 +216,12 @@ begin
    { reflexivity }
 end;
 
-symbol succ_double_carac x : π (succ_double x = double x + Zpos H) ≔
+opaque symbol succ_double_carac x : π (succ_double x = double x + Zpos H) ≔
 begin
   induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
-symbol double_succ x : π (double (x + Zpos H) = succ_double x + Zpos H) ≔
+opaque symbol double_succ x : π (double (x + Zpos H) = succ_double x + Zpos H) ≔
 begin
   induction
    { reflexivity }
@@ -235,7 +235,7 @@ symbol - x y ≔ x + — y;
 
 notation - infix left 20;
 
-symbol -_same z : π (z + — z = Z0) ≔
+opaque symbol -_same z : π (z + — z = Z0) ≔
 begin
   induction
    { reflexivity }
@@ -245,7 +245,7 @@ end;
 
 // Associativity
 
-symbol sub_succ x y : π (sub (succ x) y = sub x y + Zpos H) ≔
+opaque symbol sub_succ x y : π (sub (succ x) y = sub x y + Zpos H) ≔
 begin
   induction
   // case I
@@ -268,7 +268,7 @@ begin
      { reflexivity } }
 end;
 
-symbol add_Zpos_succ x p : π (x + Zpos (succ p) = (x + Zpos p) + Zpos H) ≔
+opaque symbol add_Zpos_succ x p : π (x + Zpos (succ p) = (x + Zpos p) + Zpos H) ≔
 begin
   induction
    { reflexivity }
@@ -276,7 +276,7 @@ begin
    { assume x p; simplify; rewrite sub_succ; reflexivity }
 end;
 
-symbol sub_add_Zpos a b c : π (sub a b + Zpos c = sub (add a c) b) ≔
+opaque symbol sub_add_Zpos a b c : π (sub a b + Zpos c = sub (add a c) b) ≔
 begin
   assume a b c;
   refine ind_ℙeano (λ c, sub a b + Zpos c = sub (add a c) b) _ _ c
@@ -287,7 +287,7 @@ begin
     rewrite add_succ_right; rewrite sub_succ; reflexivity }
 end;
 
-symbol sub_add_Zneg a b c : π (sub a b + Zneg c = sub a (add b c)) ≔
+opaque symbol sub_add_Zneg a b c : π (sub a b + Zneg c = sub a (add b c)) ≔
 begin
   assume a b c;
   rewrite left sub_opp (add b c) a;
@@ -295,7 +295,7 @@ begin
   rewrite distr_—_+; rewrite sub_opp; reflexivity;
 end;
 
-symbol +_assoc x y z : π ((x + y) + z = x + (y + z)) ≔
+opaque symbol +_assoc x y z : π ((x + y) + z = x + (y + z)) ≔
 begin
   induction
   { reflexivity }
@@ -360,7 +360,7 @@ with Zneg $p ≐ Zneg $q ↪ compare $q $p;
 
 // ≐ decides the equality of integers
 
-symbol ≐_decides x y : π (x ≐ y = Eq ⇒ x = y) ≔
+opaque symbol ≐_decides x y : π (x ≐ y = Eq ⇒ x = y) ≔
 begin
   induction
   // case Z0
@@ -384,7 +384,7 @@ end;
 
 // Commutative properties of ≐
 
-symbol ≐_com x y : π (x ≐ y = opp (y ≐ x)) ≔
+opaque symbol ≐_com x y : π (x ≐ y = opp (y ≐ x)) ≔
 begin
   induction
   // case Z0
@@ -403,7 +403,7 @@ begin
      { assume y; simplify; rewrite compare_acc_com; reflexivity } }
 end;
 
-symbol ≐_opp x y : π (— x ≐ — y = opp (x ≐ y)) ≔
+opaque symbol ≐_opp x y : π (— x ≐ — y = opp (x ≐ y)) ≔
 begin
   induction
   // case Z0
@@ -424,13 +424,13 @@ end;
 
 // General results
 
-symbol simpl_right x a : π ((x + a) - a = x) ≔
+opaque symbol simpl_right x a : π ((x + a) - a = x) ≔
 begin
   assume x a; simplify; rewrite +_assoc;
   rewrite -_same; reflexivity;
 end;
 
-symbol simpl_inv_right x a : π ((x - a) + a = x) ≔
+opaque symbol simpl_inv_right x a : π ((x - a) + a = x) ≔
 begin
   assume x a; simplify; rewrite +_assoc;
   rewrite .[— a + a] +_com; rewrite -_same; reflexivity;
@@ -438,24 +438,24 @@ end;
 
 // ≐ with 0
 
-symbol ≐_double x : π ((double x ≐ Z0) = (x ≐ Z0)) ≔
+opaque symbol ≐_double x : π ((double x ≐ Z0) = (x ≐ Z0)) ≔
 begin
   induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
-symbol ≐_pred_double x :
+opaque symbol ≐_pred_double x :
   π (pred_double x ≐ Z0 = case_Comp (x ≐ Z0) Lt Lt Gt) ≔
 begin
   induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
-symbol ≐_succ_double x :
+opaque symbol ≐_succ_double x :
   π (succ_double x ≐ Z0 = case_Comp (x ≐ Z0) Gt Lt Gt) ≔
 begin
   induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
-symbol ≐_pos_sub x y : π ((sub x y ≐ Z0) = compare x y) ≔
+opaque symbol ≐_pos_sub x y : π ((sub x y ≐ Z0) = compare x y) ≔
 begin
   induction
   // case I
@@ -476,7 +476,7 @@ begin
   { induction { reflexivity } { reflexivity } { reflexivity } }
 end;
 
-symbol ≐_sub x y : π ((x ≐ y) = (x + — y ≐ Z0)) ≔
+opaque symbol ≐_sub x y : π ((x ≐ y) = (x + — y ≐ Z0)) ≔
 begin
   induction
   // case Z0
@@ -497,7 +497,7 @@ end;
 
 // Compatibility of comparison with the addition
 
-symbol ≐_compat_add x y z : π ((x ≐ y) = (x + z ≐ y + z)) ≔
+opaque symbol ≐_compat_add x y z : π ((x ≐ y) = (x + z ≐ y + z)) ≔
 begin
   assume x y z;
   rewrite ≐_sub; rewrite .[x in _ = x] ≐_sub;
@@ -520,7 +520,7 @@ notation ≥ infix 10;
 symbol > x y ≔ ¬ (x ≤ y);
 notation > infix 10;
 
-symbol <_≤ x y : π (x < y ⇒ x ≤ y) ≔
+opaque symbol <_≤ x y : π (x < y ⇒ x ≤ y) ≔
 begin
   assume x y;
   refine ind_Comp (λ u, istrue(isLt u) ⇒ istrue(isGt u) ⇒ ⊥) _ _ _ (x ≐ y)
@@ -531,7 +531,7 @@ end;
 
 // Compatibility of directional comparison operators
 
-symbol ≤_compat_add x y a : π (x ≤ y ⇒ x + a ≤ y + a) ≔
+opaque symbol ≤_compat_add x y a : π (x ≤ y ⇒ x + a ≤ y + a) ≔
 begin
   assume x y a; simplify;
   assume H; refine fold_⇒ _; rewrite ≐_sub;
@@ -542,7 +542,7 @@ begin
   rewrite left ≐_sub x y; refine H;
 end;
 
-symbol <_compat_add x y a : π (x < y ⇒ x + a < y + a) ≔
+opaque symbol <_compat_add x y a : π (x < y ⇒ x + a < y + a) ≔
 begin
   assume x y a; simplify; assume H; rewrite ≐_sub;
   rewrite +_assoc; rewrite .[y + a] +_com;
@@ -551,7 +551,7 @@ begin
   simplify; rewrite left ≐_sub; refine H;
 end;
 
-symbol ≤_compat_≤ x y : π (Z0 ≤ x ⇒ Z0 ≤ y ⇒ Z0 ≤ x + y) ≔
+opaque symbol ≤_compat_≤ x y : π (Z0 ≤ x ⇒ Z0 ≤ y ⇒ Z0 ≤ x + y) ≔
 begin
   induction
    { assume y h H; refine H }
@@ -563,7 +563,7 @@ begin
   { assume x y f h i; refine f ⊤ᵢ }
 end;
 
-symbol <_compat_≤ x y : π (Z0 < x ⇒ Z0 ≤ y ⇒ Z0 < x + y) ≔
+opaque symbol <_compat_≤ x y : π (Z0 < x ⇒ Z0 ≤ y ⇒ Z0 < x + y) ≔
 begin
   induction
    { assume y f h; apply ⊥ₑ; refine f }
@@ -577,14 +577,14 @@ end;
 
 // Reflexivity
 
-symbol ≤_refl x : π (x ≤ x) ≔
+opaque symbol ≤_refl x : π (x ≤ x) ≔
 begin
   assume x; refine ≤_compat_add Z0 Z0 x _; refine (λ x, x);
 end;
 
 // Antisymmetry
 
-symbol ≤_antisym x y : π (x ≤ y ⇒ y ≤ x ⇒ x = y) ≔
+opaque symbol ≤_antisym x y : π (x ≤ y ⇒ y ≤ x ⇒ x = y) ≔
 begin
   assume x y;
   have e : π (¬ (istrue(isGt (x ≐ y))) ⇒ ¬ (istrue(isGt (y ≐ x))) ⇒ x = y)
@@ -598,7 +598,7 @@ end;
 
 // Transitivity theorems
 
-symbol ≤_trans x y z : π (x ≤ y ⇒ y ≤ z ⇒ x ≤ z) ≔
+opaque symbol ≤_trans x y z : π (x ≤ y ⇒ y ≤ z ⇒ x ≤ z) ≔
 begin
    assume x y z lxy lyz;
    have H : π (Z0 ≤ (z + — y) + (y + — x))
@@ -613,7 +613,7 @@ begin
    refine ≤_compat_add Z0 (z - x) x;
 end;
 
-symbol <_trans_1 x y z : π (x < y ⇒ y ≤ z ⇒ x < z) ≔
+opaque symbol <_trans_1 x y z : π (x < y ⇒ y ≤ z ⇒ x < z) ≔
 begin
   assume x y z lxy lyz;
   have H : π (Z0 < (z + — y) + (y + — x))
@@ -627,7 +627,7 @@ begin
   refine <_compat_add Z0 (z - x) x;
 end;
 
-symbol <_trans_2 x y z : π (x ≤ y ⇒ y < z ⇒ x < z) ≔
+opaque symbol <_trans_2 x y z : π (x ≤ y ⇒ y < z ⇒ x < z) ≔
 begin
   assume x y z lxy lyz;
   have H : π (Z0 < (z + — y) + (y + — x))