proposition: Lemma build_z_atom_correct : forall a z, build_z_atom a = Some z -> interp_atom a = Bval t_i Typ.TZ z.
proof: Proof. apply build_z_atom_aux_correct. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz