proposition: Lemma valid_check_False : C.valid rho check_False.
proof: Proof. unfold check_False, C.valid. change (Lit.interp rho (Lit.neg Lit._false) || false = true). rewrite Lit.interp_neg. assert (W:= Lit.interp_false _ Hwfrho). destruct (Lit.interp rho Lit._false);trivial;elim W;red;trivial. Qed.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList