proposition: Lemma i_eqb_t : forall t x y, i_eqb t x y = i_eqb_eqb t x y.
proof: Proof. intros. unfold i_eqb_eqb. destruct t; simpl; auto; unfold i_eqb; simpl. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList