-(* 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. *)
+(* 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. *)