proposition: Lemma i_eqb_spec_false : forall t x y, i_eqb t x y = false <-> x <> y.
proof: Proof. intros. unfold i_eqb. apply eqb_compdec_spec_false. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList