proposition: Lemma eqb_compdec_refl {t} (c : CompDec t) : forall x, eqb_of_compdec c x x = true.
proof: Proof. intro x. apply eqb_refl. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList