fact: Definition interp_form_hatom_bv t_atom : hatom -> forall s, BITVECTOR_LIST.bitvector s := let interp := interp_hatom t_atom in fun a s => interp_bv (interp a) s.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList