proposition: Lemma build_z_correct : forall h z, build_z h = Some z -> t_interp.[h] = Bval t_i Typ.TZ z.
proof: Proof. unfold build_z;intros h z;rewrite t_interp_wf;trivial. apply build_z_atom_aux_correct;discriminate. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz