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