fact: Hypothesis valid_check_step : forall s, S.valid rho s -> forall c, S.valid rho (check_step s c).
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker