+(* comparing lists *)
+
+lemma compare_append : ∀A,l1,l2,l3,l4. l1@l2 = l3@l4 →
+∃l:list A.(l1 = l3@l ∧ l4=l@l2) ∨ (l3 = l1@l ∧ l2=l@l4).
+#A #l1 elim l1
+ [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
+ |#a1 #tl1 #Hind #l2 #l3 cases l3
+ [#l4 #Heq %{(a1::tl1)} %1 % // @sym_eq @Heq
+ |#a3 #tl3 #l4 normalize in ⊢ (%→?); #Heq cases (Hind l2 tl3 l4 ?)
+ [#l * * #Heq1 #Heq2 %{l}
+ [%1 % // >Heq1 >(cons_injective_l ????? Heq) //
+ |%2 % // >Heq1 >(cons_injective_l ????? Heq) //
+ ]
+ |@(cons_injective_r ????? Heq)
+ ]
+ ]
+ ]
+qed.