fact: Definition wf_vmap (vm:vmap) := (List.length (snd vm) = nat_of_P (fst vm) - 1)%nat /\ List.forallb (fun h => check_atom h Typ.TZ) (snd vm).
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz