proposition: Lemma _checker__correct : forall s, forall t confl, _checker_ s t confl-> ~ (S.valid rho s).
proof: Proof. unfold _checker_. intros s t' cid Hf Hv. apply (is_false_correct Hf). apply S.valid_get. clear Hf. rewrite <- List.fold_left_rev_right in *. induction (List.rev (fst t')); [ apply Hv | ]. apply valid_check_step. apply IHl. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker