fact: Definition BoundedString_eq_dec {n} {Bound} (bidx bidx' : BoundedString Bound) : {bidx = bidx'} + {bidx <> bidx'} := @BoundedIndex_eq_dec _ n Bound bidx bidx'.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2