proposition: Lemma eval_fold_update_correct : forall m concl F (FOK : forall st cl, has_watched_clause m cl -> eval_watched_clause cl -> wf_state st ->eval_state st -> wf_result_state (F cl st) /\ eval_result_state (F cl st)) acc st (WF: Forall (has_watched_clause m) acc) (EC: Forall eval_watched_clause acc) (WS: wf_state st) (ES: eval_state st), (eval_result_state (fold_update F acc st) -> eval_formula concl) -> eval_formula concl.
proof: Proof. induction acc; simpl. - tauto. - intros. inv WF. inv EC. specialize (FOK _ _ H2 H4 WS ES). destruct (F a st) ; simpl in *; try tauto. destruct FOK. eapply IHacc with (st:=st0); eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause