proposition: Lemma build_z_atom_aux_correct : forall a z, build_z_atom_aux a = Some z -> interp_atom a = Bval t_i Typ.TZ z.
proof: Proof. intros a z. destruct a;simpl;try discriminate;auto. destruct c;[discriminate | intros Heq;inversion Heq;trivial | discriminate]. destruct u;try discriminate; case_eq (build_positive i);try discriminate; intros p Hp Heq;inversion Heq;clear Heq;subst; rewrite (build_positive_correct _ _ Hp);trivial. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz