proposition: Lemma eval_pset_remove : forall m a s (HF : has_literal m a) (HLIT: has_lit a s = true) (WFS: wf_pset m s) , eval_literal a -> eval_pset m (remove_lit a s) -> eval_pset m s.
proof: Proof. intros. unfold eval_pset in *. intros. assert (HREM:= H0 f b H1). unfold remove_lit, LitSet.get, LitSet.remove in HREM, H1. unfold has_lit in *. rewrite grspec in HREM by (destruct WFS;auto). destruct (eqs (id f) (id_of_literal a)). - assert (f = form_of_literal a). { apply has_form_eq with (m:=m) ;auto. apply has_form_of_literal; auto. } subst. clear HREM. rewrite e in *. destruct ((LitSet.get (id_of_literal a) s)); try congruence. destruct t0 ; try congruence. unfold OBool.lift_has_bool in H2. simpl in *. rewrite eqb_true_iff in *. subst. rewrite literal_eq; auto. - apply HREM;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause