proposition: Corollary idx_ibound_eq : forall n Bound (idx idx' : BoundedIndex (n := n) Bound), ibound (indexb idx) = ibound (indexb idx') -> idx = idx'.
proof: Proof. intros; generalize (@indexb_ibound_eq _ _ idx idx' H); destruct idx as [idx [n' In_n'] ]; destruct idx' as [idx' [n'' In_n'' ] ]; intros; simpl in *; subst; f_equal. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2