proposition: Lemma build_positive_correct : forall h p, build_positive h = Some p -> t_interp.[h] = Bval t_i Typ.Tpositive p.
proof: Proof. unfold build_positive. apply foldi_ind;intros;try discriminate. apply leb_0. rewrite t_interp_wf;trivial. apply (build_positive_atom_aux_correct a); trivial. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz