proposition: Lemma fold_update_correct : forall {A: Type} (F: A -> state -> dresult) (Q: state -> A -> Prop) l (QOK : forall a st st', F a st = Progress st' -> forall x, Q st x -> Q st' x) (FOK : forall a st, Q st a -> wf_state st -> wf_result_state (F a st)) st (QALL : Forall (Q st) l) (Acc : wf_state st), wf_result_state (fold_update F l st).
proof: Proof. induction l; simpl. - auto. - intros. inv QALL. generalize (FOK _ _ H1 Acc). destruct (F a st) eqn:EQ; simpl; auto. apply IHl; auto. revert H2. apply Forall_Forall. intros. eapply QOK ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause