+(* Let us conclude this section with a discussion of the notation for the
+existential quantifier. *)
+
+notation "hvbox(\exists ident i : ty break . p)"
+ right associative with precedence 20 for
+ @{'exists (\lambda ${ident i} : $ty. $p) }.
+
+(* The main novelty is the special keyword "ident" that instructs the system
+that the variable i is expected to be an identifier. Matita abstract syntax
+trees include lambda terms as primitive data types, and the previous declaration
+simply maps the notation ∃x.P into a content term of the form ('exists (λx.p))
+where p is the content term obtained from P.
+
+The corresponding interpretation is then straightforward: *)
+
+interpretation "exists" 'exists x = (ex ? x).
+
+(* The notational language of Matita has an additional list operator for dealing
+with variable-size terms having a regular structure. Such operator has a
+corresponding fold operator, to build up trees at the content level.
+
+For example, in the case of quantifiers, it is customary to group multiple
+variable declarations under a same quantifier, writing e.g. ∃x,y,z.P instead of
+∃x.∃y.∃z.P.
+
+This can be achieved by the following notation: *)
+
+notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
+ }.
+
+(* The presentational pattern matches terms starting with the existential
+symbol, followed by a list of identifiers separated by commas, optionally
+terminated by a type declaration, followed by a fullstop and finally by the body
+term. We use list1 instead of list0 since we expect to have at least one
+identifier: conversely, you should use list0 when the list can possibly be
+empty.
+
+The "default" meta operator at content level matches the presentational opt and
+has two branches, which are chosen depending on the matching of the optional
+subexpression. Let us consider the first, case, where we have
+an explicit type. The content term is build by folding the function
+
+ rec acc @{'exists (λ${ident x}:$T.$acc)}
+
+(where "rec" is the binder, "acc" is the bound variable and the rest is the
+body) over the initial content expression @{$Px}. *)
+
+lemma distr_and_or_l : ∀A,B,C:Prop. A ∧(B ∨ C) → (A ∧ B) ∨ (A ∧ C).
+#A #B #C * #H *
+ [#H1 %1 % [@H |@H1] |#H1 %2 % //]
+qed.
+
+lemma distr_and_or_r : ∀A,B,C:Prop. (A ∧ B) ∨ (A ∧ C) → A ∧ (B ∨ C).
+#A #B #C * * #H1 #H2
+ [% [// | %1 //] | % [// | %2 //]
+qed.
+
+
+lemma distr_or_and_l : ∀A,B,C:Prop. A ∨(B ∧ C) → (A ∨ B) ∧ (A ∨ C).
+#A #B #C *
+ [#H % [%1 // |%1 //] | * #H1 #H2 % [%2 // | %2 //] ]
+qed.
+
+lemma distr_or_and_r : ∀A,B,C:Prop. (A ∨ B) ∧ (A ∨ C) → A ∨ (B ∧ C).
+#A #B #C
+* * #H * /3/
+qed.
+
+definition neg ≝ λA:Prop. A → False.
+
+lemma neg_neg : ∀A. A → neg (neg A).
+#A #H normalize #H1 @(H1 H)
+qed.
+
+(***************************** Leibniz Equality *******************************)
+
+(* Even equality is a derived notion in Matita, and a particular case of an
+inductive type. The idea is to define it as the smallest relation containing
+reflexivity (that is, as the smallest reflexive relation over a given type). *)
+
+inductive eq (A:Type[0]) (x:A) : A → Prop ≝
+ refl: eq A x x.
+
+(* We can associate the standard infix notation for equality via the following
+declarations: *)
+
+notation "hvbox(a break = b)"
+ non associative with precedence 45 for @{ 'eq ? $a $b }.
+
+interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+
+(* The induction principle eq_ind automatically generated by the system
+(up to dependencies) has the following shape:
+
+ ∀A:Type[0].∀x:A. ∀P:A→Prop. P x → ∀y:A. x = y → P y
+
+This principle is usually known as ``Leibniz equality'': two objects x and y are
+equal if they cannot be told apart, that is for any property P, P x implies P y.
+
+As a simple exercise, let us also proof the following variant: *)
+
+lemma eq_ind_r: ∀A:Type[0].∀x:A. ∀P:A→Prop. P x → ∀y:A. y = x → P y.
+#A #x #P #Hx #y #eqyx <eqyx in Hx; // qed.
+
+(* The order of the arguments in eq_ind may look a bit aleatoric but, as we shall
+see, it is motivated by the underlying structure of the inductive type.
+Before discussing the way eq_ind is generated, it is time to make an important
+discussion about the parameters of inductive types.
+
+If you look back at the definition of equality, you see that the first argument
+x has been explicitly declared, together with A, as a formal parameter of the
+inductive type, while the second argument has been left implicit in the
+resulting type A → Prop. One could wonder if this really matters, and in
+particular if we could use the following alternative definitions:
+
+ inductive eq1 (A:Type[0]) (x,y:A) : Prop ≝
+ refl1: eq1 A x x.
+
+ inductive eq2 (A:Type[0]): A → A → Prop ≝
+ refl2: ∀x.eq2 A x x.
+
+The first one is just wrong. If you try to type it, you get the following error
+message: ``CicUnification failure: Can't unify x with y''.
+The point is that the role of parameters is really to define a family of types
+uniformly indexed over them. This means that we expect all occurrences of the
+inductive type in the type of constructors to be precisely instantiated with the
+input parameters, in the order they are declared. So, if A,x and y are
+parameters for eq1, then all occurrences of this type in the type of
+constructors must have be of the kind eq1 A x y (while we have eq1 A x x, that
+explains the typing error).
+
+If you cannot express an argument as a parameter, the only alternative is to
+implicitly declare it in the type of the inductive type.
+Henceforth, when we shall talk about ``arguments'' of inductive types, we shall
+implicitly refer to arguments which are not parameters (sometimes, people call
+them ``right'' and ``left'' parameters, according to their position w.r.t the
+double points in the type declaration. In general, it is always possible to
+declare everything as an argument, but it is a very good practice to shift as
+many argument as possible in parameter position. In particular, the definition
+of eq2 is correct, but the corresponding induction principle eq2_ind is not as
+readable as eq_ind. *)
+
+inductive eq2 (A:Type[0]): A → A → Prop ≝
+ refl2: ∀x.eq2 A x x.
+
+(* The elimination rule for a (non recusive) inductive type T having a list
+of parameters A1,…,An and a list of arguments B1,…,Bm, has the following shape
+(still, up to dependencies):
+
+ ∀a1:A1,… ∀an:An,∀P:B1 → … → Bm → Prop.
+ C1 → … → Ck → ∀x1:B1…∀xm:Bm.T a1 … an b1 … bm → P x1 … xm
+
+where Ci is obtained from the type Ti of the constructor ci replacing in it each
+occurrence of (T a1 … an t1 … tm) with (P t1 … tm).
+
+For instance, eq2 only has A as parameter, and two arguments.
+The corresponding elimination principle eq2_ind is as follows:
+
+ ∀A:Type[0].∀P:A → A → Prop. ∀z.P z z → ∀x,y:A. eq2 A x y → P x y
+
+As we prove below, eq2_ind and eq_ind are logically equivalent (that is, they
+mutually imply each other), but eq2_ind is slighty more complex and innatural.