proposition: Lemma eqb_compdec_trans {t} (c : CompDec t) : forall x y z, eqb_of_compdec c x y = true -> eqb_of_compdec c y z = true -> eqb_of_compdec c x z = true.
proof: Proof. intros x y z. apply eqb_trans. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList