proposition: Lemma not_eq_cons : forall (l1 l2 : list A) (a1 a2 : A), l1 <> l2 -> a1 :: l1 <> a2 :: l2.
proof: Proof. red in |- *. intros. absurd (l1 = l2). exact H. apply (eq_cons l1 l2 a1 a2). exact H0. Qed.
imports: List Arith_compl