proposition: Lemma wf_unsat : forall m l u d (AN : wf_pset m (Annot.deps l)) (WFU : wf_units_lit u m) (US : is_unsat u l = Some d), wf_pset m d.
proof: Proof. unfold is_unsat in *. intros. destruct (Annot.elt l). destruct (is_hFF f). inv US. auto. destruct (IntMap.get' (id f) u) eqn:EQ; try congruence. apply WFU in EQ. destruct (Annot.lift negb t0); try congruence. inv US. apply wf_pset_union;auto. tauto. destruct (IntMap.get' (id f) u) eqn:EQ; try congruence. apply WFU in EQ. destruct (Annot.elt t0); try congruence. inv US. apply wf_pset_union;auto. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause