proposition: Lemma subset_reduce_lits : forall u m (WFU: wf_units_lit u m) cl an (WF: wf_map an) , ohold (fun x => wf_map (Annot.deps x) /\ LitSet.subset an (Annot.deps x)) (reduce_lits u an cl).
proof: Proof. induction cl. - simpl. intro. split ; auto. unfold LitSet.subset. intros. destruct (LitSet.get k an) ; simpl ; auto. apply OBool.order_refl. - simpl. intros. destruct (find_lit a u) eqn:EQ. + apply check_annot_find_lit with (hm:=m) in EQ; auto. destruct (Annot.elt t0);simpl ; auto. specialize (IHcl ((LitSet.union (Annot.deps t0) an))). destruct ((reduce_lits u (LitSet.union (Annot.deps t0) an) cl)); simpl in *; auto. assert (WFM : wf_map (LitSet.union (Annot.deps t0) an)). { apply LitSet.wf_union;auto. destruct EQ;auto. } specialize (IHcl WFM). destruct IHcl. split ; auto. eapply LitSet.subset_trans ; eauto. apply LitSet.subset_union_r;auto. destruct EQ ; auto. + specialize (IHcl _ WF). destruct (reduce_lits u an cl); simpl; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause