proposition: Lemma eval_annot_fold_update : forall {A: Type} (EVAL : A -> Prop) (WP : hmap -> A -> Prop) F l (WPI : forall m m', hmap_order m m' -> forall x, WP m x -> WP m' x) (FO : Forall (fun cl => forall st,wf_state st -> eval_annot_state st ->WP (hconsmap st) cl -> hconsmap_progress (F cl) st /\ wf_result_state (F cl st) /\ eval_annot_result_state (F cl st)) l) st (WF : wf_state st) (ES : eval_annot_state st) (ALL : Forall (WP (hconsmap st)) l) (CLS : Forall EVAL l), eval_annot_result_state (fold_update F l st).
proof: Proof. induction l ; simpl; auto. intros. inv CLS. inv ALL. inv FO. specialize (H5 _ WF ES). destruct (H5 H3) as (HH1 & HH2 & HH3). unfold hconsmap_progress in *. destruct (F a st) ; simpl in * ; auto. eapply IHl ; eauto. revert H4. apply Forall_Forall; auto. apply WPI. intuition congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause