Incoherence of definitions in tutorial and arend-lib

[sxhya]

trafficstars

Some definitions given in the tutorial have differently defined counterparts with the same name from arend-lib.

1. in the tutorial || is the non-truncated definition, but in arend-lib it is truncated, so it can not be used for pattern-matching in the same fashion due to homotopy level checking. Probably Set/Prop variations of basic operators such as && or || should be given names in a similar fashion to Coq/Ssreflect (see any of their tutorials).
2. Fin n is currently built into Arend.Prelude, so it makes sense to additionally explain how to work with current implementation of Fin n. The definition with fzero and fsuc can be left in the tutorial for illustrative purposes, but probably should be renamed and supplied with a commentary.
3. < in tutorial is a boolean function similar to an auxiliary function Arith.Prime but < in Arith.Nat is a completely different datatype. Probably some renaming or comment is needed.