proposition: Lemma i_eqb_trans : forall t x y z, i_eqb t x y -> i_eqb t y z -> i_eqb t x z.
proof: Proof. intros. unfold i_eqb. apply (eqb_compdec_trans _ x y z); auto. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList