proposition: Lemma theorem_checker : forall d c, checker d c = true -> forall rho, ~ (valid (interp_var rho) d).
proof: Proof. intros d c H rho;apply checker_correct with c;trivial. split;compute;trivial;discriminate. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker