proposition: Lemma wf_make_clause : forall m u cl an (WFU: wf_units_lit u m) (WFA: wf_pset m an) (HAS: has_conflict_clause m cl), check_annot has_clause m (make_clause u an cl).
proof: Proof. induction cl; simpl; auto. - intros. split; auto. constructor. - intros. destruct (find_lit a u) eqn:EQ; simpl ; intros. destruct (Annot.elt t0). + apply check_annot_TRUE. + apply IHcl; auto. apply wf_pset_union;auto. apply check_annot_find_lit with (hm:=m) in EQ;auto. inv HAS;auto. + inv HAS. apply check_annot_reduce; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause