proposition: Lemma eval_pset_singleton : forall m f b (HF : has_form m f), eval_pset m (LitSet.singleton (id f) b) -> eval_literal (literal_of_bool b f).
proof: Proof. intros. apply H; auto. unfold LitSet.get, LitSet.singleton. simpl. rewrite eqb_refl. unfold OBool.lift_has_bool. simpl. apply Bool.eqb_reflx. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause