proposition: Lemma has_no_dup_clause : forall hm l (HL: Forall (has_literal hm) l), has_clause hm (no_dup_clause l).
proof: Proof. induction l ; simpl; auto. destruct l. - simpl. intros. inv HL; auto. - destruct_in_goal EL. + intros. inv HL ; apply IHl;auto. + intros. simpl. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause