proposition: Lemma eqb_compdec_spec {t} (c : CompDec t) : forall x y, eqb_of_compdec c x y = true <-> x = y.
proof: Proof. intros x y. destruct c as [TY [E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList