+(* The definition starts with the keyword "inductive" followed by the name we
+want to give to the new datatype (in this case, "bank"), followed by its type (a
+type of a type is traditionally called a "sort" in type theory). We have
+basically two sorts in Matita: "Prop" and "Type". "Prop" is meant for logical
+propositions, while "Type" should be used for dataypes (we shall tell more about
+the attribute $0$ in a later Section).
+
+The definition proceeds with the keyword ``:='' (or "\def") followed by the
+"body" of the definition. The body is just a list of "constructors" for the
+inductive type, separated by the keyword | (vertical bar). Each constructor is a
+pair composed by a name and its type. Constructors (in our case, "east" and
+"west") are the "canonical inhabitants" of the inductive type we are defining
+(in our case, "bank"), hence their type must be of type "bank".
+In general, as we shall see, constructors for an inductive type T may have a
+more complex structure, and in particular can be recursive: the general proviso
+is that they must always "return" a result of type T.
+Hence, the declaration of a constructor c for and inductive type T has the
+following typical shape:
+ A1 → … → An → T
+where A1 … A_n can be arbitrary types, comprising T itself. Not every form of
+recursive constructors is accepted however: in order to ensure logical
+consistency, we must respect some positivity conditions, that we shall discuss
+in Section ??.
+
+As a general rule, the inductive type must be conceptually understood as the
+smallest collection of terms freely generated by its constructors. *)
+
+(********************************* functions **********************************)
+
+(* We define a first simple function computing, for each bank of the river, the