proposition: Lemma no_dup_clause_correct : forall hm cl (WF: Forall (has_literal hm) cl), eval_literal_list cl -> eval_clause (no_dup_clause cl).
proof: Proof. intros. induction WF. - constructor. - simpl. destruct l. + simpl in *. destruct x ; simpl in *. tauto. auto. + destruct_in_goal SL. replace x with l in *. simpl in H. rewrite eval_literal_same in H. auto. symmetry. inv WF. eapply has_literal_eq;eauto. simpl. unfold eval_watched_clause. simpl. apply H;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause