proposition: Lemma leibniz_eq_Z_B2P: forall x y, eqP_Z x y <-> Logic.eq x y.
proof: Proof. intros x y; split; intro H. unfold eqP_Z in H. case_eq ((x =? y)%Z); intros. now apply Z.eqb_eq in H0. rewrite H0 in H. now contradict H. rewrite H. unfold eqP_Z. now rewrite Z.eqb_refl. Qed.
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes