proposition: Lemma valid_check_BuildDef2 : forall l, C.valid rho (check_BuildDef2 l).
proof: Proof. unfold check_BuildDef2,C.valid;intros l. case_eq (t_form.[Lit.blit l]);intros;auto using C.interp_true; case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl; tauto_check. Qed.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList