proposition: Lemma eval_pset_subset : forall m an an', LitSet.subset an an' -> eval_pset m an' -> eval_pset m an.
proof: Proof. unfold eval_pset. intros. apply H0; auto. unfold LitSet.subset in *. specialize (H (id f)). unfold OBool.lift_has_bool in *. destruct (LitSet.get (id f) an) , (LitSet.get (id f) an') ; simpl in *; intuition try congruence. - eapply has_boolb_mono ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause