fact: Definition top_eqb o o' := match o, o' with | TO_store ti te, TO_store ti' te' => Typ.eqb ti ti' && Typ.eqb te te' end.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList