fact: Definition interp_bool (v:bval) : bool := let (t,v) := v in match Typ.cast t Typ.Tbool with | Typ.Cast k => k _ v | _ => true end.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList