proposition: Lemma reflect_eqb_compdec {t} (c : CompDec t) : forall x y, reflect (x = y) (eqb_of_compdec c x y).
proof: Proof. intros x y. apply SMT_classes.reflect_eqb. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList