proposition: Lemma build_positive_atom_correct : forall (a:atom) (p:positive), build_positive_atom a = Some p -> interp_atom a = Bval t_i Typ.Tpositive p.
proof: Proof. apply build_positive_atom_aux_correct;apply build_positive_correct. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz