+(* Functions are live entities, and can be actually computed. To check this, let
+us state the property that the opposite bank of east is west; every lemma needs a
+name for further reference, and we call it "east_to_west". *)
+
+lemma east_to_west : \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6.
+
+(* If you stop the execution here you will see a new window on the right side
+of the screen: it is the goal window, providing a sequent like representation of
+the form
+
+B1
+B2
+....
+Bk
+-----------------------
+A
+
+for each open goal remaining to be solved. A is the conclusion of the goal and
+B1, ..., Bk is its context, that is the set of current hypothesis and type
+declarations. In this case, we have only one goal, and its context is empty.
+The proof proceeds by typing commands to the system. In this case, we
+want to evaluate the function, that can be done by invoking the "normalize"
+command:
+*)
+
+normalize
+
+(* By executing it - just type the advance command - you will see that the goal
+has changed to west = west, by reducing the subexpression (opposite east).
+You may use the retract bottom to undo the step, if you wish.
+
+The new goal west = west is trivial: it is just a consequence of reflexivity.
+Such trivial steps can be just closed in Matita by typing a double slash.
+We complete the proof by the qed command, that instructs the system to store the
+lemma performing some bookkeeping operations.
+*)
+