-(* As an application of the previous result let us prove that l1@l2 is empty if and
-only if both l1 and l2 are empty. The idea is to proceed by cases on l1: if l1=[] the
-statement is trivial; on the other side, if l1 = a::tl, then the hypothesis
-(a::tl)@l2 = [] is absurd, hence we can prove anything from it. When we know we can
-prove both A and ¬A, a sensible way to proceed is to apply False_ind: ∀P.False → P to the
-current goal, that breaks down to prove False, and then absurd: ∀A:Prop. A → ¬A → False
-to reduce to the contradictory cases. Usually, you may invoke automation to take care
-to solve the absurd case. *)
-
-lemma nil_to_nil: ∀A.∀l1,l2:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6A.
- l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
-#A #l1 cases l1 normalize /2/ #a #tl #l2 #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ qed.
-
-(* Let us come to some important, higher order, polymorphic functionals
+(* As an application of the previous result let us prove that l1@l2 is empty if
+and only if both l1 and l2 are empty.
+The idea is to proceed by cases on l1: if l1=[] the statement is trivial; on the
+other side, if l1 = a::tl, then the hypothesis (a::tl)@l2 = [] is absurd, hence we
+can prove anything from it.
+When we know we can prove both A and ¬A, a sensible way to proceed is to apply
+False_ind: ∀P.False → P to the current goal, that breaks down to prove False, and
+then absurd: ∀A:Prop. A → ¬A → False to reduce to the contradictory cases.
+Usually, you may invoke automation to take care to solve the absurd case. *)
+
+\ 5img class="anchor" src="icons/tick.png" id="nil_to_nil"\ 6lemma nil_to_nil: ∀A.∀l1,l2:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6A.
+ l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
+#A #l1 cases l1 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ #a #tl #l2 #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+(*
+\ 5h2 class="section"\ 6Higher Order Functionals\ 5/h2\ 6
+Let us come to some important, higher order, polymorphic functionals