proposition: Lemma discr : forall {A:Type} (a: A), a::nil = nil -> a::nil = a::nil -> False.
proof: Proof. intros. itauto congruence. Qed.
imports: Cdcl.Itauto Uint63 Bool ZArith Lia Coq.Lists.List Coq.ZArith.ZArith Coq.micromega.Lia Bool ZifyClasses Coq.ZArith.ZArith Coq.micromega.Lia Classical