proposition: Lemma valid_set_resolve : forall rho s, Valuation.wf rho -> valid rho s -> forall pos r, valid rho (set_resolve s pos r).
proof: Proof. unfold set_resolve; intros rho s Hrho Hv pos r. destruct (reflect_eqb (length r) 0);[trivial | ]. apply valid_internal_set;trivial. pattern (length r); apply (int_ind_bounded _ 1). generalize (to_Z_bounded (length r)); rewrite <- to_Z_eq, to_Z_0 in n; rewrite leb_spec, to_Z_1; lia. rewrite foldi_ge; [ apply Hv | reflexivity ]. intros i Hi1 Hi2 Hc. rewrite foldi_lt_r. apply C.resolve_correct; [ apply Hv | ring_simplify (i + 1 - 1); exact Hc ]. rewrite ltb_spec, to_Z_add_1_wB, to_Z_1. rewrite leb_spec, to_Z_1 in Hi1; generalize (to_Z_bounded i); lia. rewrite ltb_spec in Hi2; generalize (to_Z_bounded (length r)); lia. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring