proposition: Lemma fold_update_not_OutOfFuel : forall {A: Type} (F: A -> state -> dresult) (FOUT : forall a st, ~ is_fail (F a st)), forall l st, ~ is_fail (fold_update F l st).
proof: Proof. induction l; simpl. - congruence. - intros. generalize (FOUT a st). destruct (F a st) eqn:EQ; try congruence. intros. apply IHl. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause