proposition: Lemma reflect_i_eqb : forall t x y, reflect (x = y) (i_eqb t x y).
proof: Proof. intros. unfold i_eqb. apply reflect_eqb_compdec. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList