add doc and a few other things (#8)

- add ssr documentation in Nat and List
- Eq: add eq_sym
- List: change notation for concatenation to ++
- Nat: replace zero by 0, and p by postfix -1
- Nat: add lemmas on 2* and even/odd numbers
- Set: add projections for cartesian product

Author: fblanqui

Bool.lp

@@ -2,11 +2,12 @@
 
 require open Blanqui.Lib.Set Blanqui.Lib.Prop Blanqui.Lib.FOL Blanqui.Lib.Eq;
 
-inductive 𝔹 : TYPE ≔
+inductive 𝔹 : TYPE ≔ // `dB or \BbbB
 | true : 𝔹
 | false : 𝔹;
 
 constant symbol bool : Set;
+
 rule τ bool ↪ 𝔹;
 
 // induction principle with equalities
@@ -159,3 +160,4 @@ symbol if : 𝔹 → Π [a], τ a → τ a → τ a;
 
 rule if true  $x _ ↪ $x
 with if false _ $y ↪ $y;
+

Eq.lp

@@ -25,3 +25,8 @@ opaque symbol feq2 [a b c] (f:τ a → τ b → τ c):
 begin
   assume a b c f x x' xx' y y' yy'; rewrite xx'; rewrite yy'; reflexivity
 end;
+
+opaque symbol eq_sym [a] [x y:τ a] : π(x = y) → π(y = x) ≔
+begin
+  assume a x y h; symmetry; apply h
+end;

FOL.lp

@@ -4,17 +4,13 @@ require open Blanqui.Lib.Set Blanqui.Lib.Prop;
 
 // Universal quantification
 
-constant symbol ∀ [a] : (τ a → Prop) → Prop;
-
-notation ∀ quantifier;
+constant symbol ∀ [a] : (τ a → Prop) → Prop; notation ∀ quantifier; // !! or \forall
 
 rule π (∀ $f) ↪ Π x, π ($f x);
 
 // Existential quantification
 
-constant symbol ∃ [a] : (τ a → Prop) → Prop;
-
-notation ∃ quantifier;
+constant symbol ∃ [a] : (τ a → Prop) → Prop; notation ∃ quantifier; // ?? or \exists
 
 constant symbol ∃ᵢ [a] p (x:τ a) : π (p x) → π (∃ p);
 symbol ∃ₑ [a] p : π (∃ p) → Π q, (Π x:τ a, π (p x) → π q) → π q;