-@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /2/
-@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"\ 6move_cabbage\ 5/a\ 6 ?? \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 … )) /2/
-@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"\ 6move_boat\ 5/a\ 6 ??? \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 …)) /2/
-@\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6 /2/
-qed.
\ No newline at end of file
+lemma opposite_to_opp: ∀a,b. a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 b → \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 a b.
+
+(* As usual, we start introducing a, b and the hypothesis (a = opposite b),
+that we call eqa. *)
+
+#a #b #eqa
+
+(* The right way to proceed, now, is by rewriting a into (opposite b). We do
+this by typing ">eqa". If we wished to rewrite in the opposite direction, namely
+opposite b into a, we would have typed "<eqa". *)
+
+>eqa
+
+(* We conclude the proof by cases on b. *)
+
+cases b // qed.
+
+(* Let's do now an important remark.
+Let us state again the problem of the goat, the wolf and the cabbage, and let
+us retry to run automation. *)
+
+lemma problem_bis: \ 5a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"\ 6reachable\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/start.def(1)"\ 6start\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/end.def(1)"\ 6end\ 5/a\ 6.
+normalize /9/
\ No newline at end of file