proposition: Lemma indexb_ibound_eq : forall n Bound (bidx bidx' : BoundedIndex (n := n) Bound), ibound (indexb bidx) = ibound (indexb bidx') -> bindex bidx = bindex bidx'.
proof: Proof. intros; induction Bound; simpl in *. - apply BoundedIndex_nil; auto. - destruct bidx as [bindex [n' nth_n] ]; destruct bidx' as [bindex' [n'' nth_n'] ]; simpl in *; subst. congruence. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2