-definition a ≝ \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"\ 6s\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"\ 6DeqNat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
-definition b ≝ \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"\ 6s\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"\ 6DeqNat\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6).
-definition c ≝ \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"\ 6s\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"\ 6DeqNat\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6)).
+\ 5img class="anchor" src="icons/tick.png" id="a"\ 6definition a ≝ \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"\ 6s\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"\ 6DeqNat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="b"\ 6definition b ≝ \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"\ 6s\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"\ 6DeqNat\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6).
+\ 5img class="anchor" src="icons/tick.png" id="c"\ 6definition c ≝ \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"\ 6s\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"\ 6DeqNat\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6)).