proposition: Lemma wf_pset_reduce : forall u m cl d l (WFU : wf_units_lit u m) (WFP : wf_pset m d), wf_pset m (Annot.deps (reduce u d l cl)).
proof: Proof. induction cl. - simpl; auto. - simpl. intros. destruct_in_goal SL. auto. destruct_in_goal FD. + apply check_annot_find_lit with (hm:=m) in FD ; auto. destruct_in_goal A. apply wf_pset_empty. apply IHcl; auto. apply wf_pset_union;auto. + simpl; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause