proposition: Lemma nodup_nil : forall {A: Type} (dec : forall (x y:A), {x = y} + {x <> y}) l, nodup dec l = nil -> l = nil.
proof: Proof. induction l. - reflexivity. - simpl. destruct (in_dec dec a l). intro. apply IHl in H. subst. simpl in i. tauto. discriminate. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause