proposition: Lemma valid_add_roots : forall rho, Valuation.wf rho -> forall d s, valid rho d -> S.valid rho s -> S.valid rho (add_roots s d).
proof: Proof. intros rho Hwr d s Hd Hs; unfold add_roots. apply (foldi_ind _ (fun _ a => S.valid rho a)); [ apply leb_0 | | ]; auto; intros i a _ Hle Hv; apply S.valid_set_clause; auto; rewrite valid_spec in Hd; apply Hd; auto. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker