proposition: Lemma eq_cons : forall (l1 l2 : list A) (a1 a2 : A), a1 :: l1 = a2 :: l2 -> l1 = l2.
proof: Proof. intros. change (tail (a1 :: l1) = tail (a2 :: l2)) in |- *. apply (f_equal (A:=list A)). exact H. Qed.
imports: List Arith_compl