proposition: Corollary idx_ibound_neq : forall n Bound (idx idx' : BoundedIndex (n := n) Bound), ibound (indexb idx) <> ibound (indexb idx') -> idx <> idx'.
proof: Proof. intros; destruct idx as [idx [n' In_n' ] ]; destruct idx' as [idx' [n'' In_n'' ] ]; intros; simpl in *; subst. unfold not; intros; apply H; injection H0; auto. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2