proposition: Lemma has_cardinal_no_dup : forall {A: Type} (l:list A), NoDup l -> has_cardinal l (length l).
proof: Proof. intros. induction H. - simpl. constructor. - simpl. constructor;auto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause