proposition: Lemma valid_check_ImmBuildDef2 : forall cid, C.valid rho (check_ImmBuildDef2 cid).
proof: Proof. unfold check_ImmBuildDef2,C.valid;intros cid. generalize (Hs cid);unfold C.valid. destruct (S.get s cid) as [ | l [ | _l _c]];auto using C.interp_true. simpl;unfold Lit.interp, Var.interp; rewrite !rho_interp; destruct (t_form.[Lit.blit l]);auto using C.interp_true; case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; tauto_check. Qed.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList