proposition: Lemma ilist2_eq {m} {B : A -> Type} : forall (Bound : Vector.t A m) (il il' : ilist2 (B := B) Bound), (forall idx, ith_Bounded2 il idx = ith_Bounded2 il' idx) -> il = il'.
proof: Proof. induction Bound; intros. - rewrite (ilist2_invert _ il), (ilist2_invert _ il'); reflexivity. - destruct il; destruct il'; simpl in *. f_equal. + generalize (H {| bindex := h |}); unfold ith_Bounded2; simpl; auto. + apply IHBound; intros. exact (H {| bindex := bindex idx; indexb := @Build_IndexBound _ (S n) (bindex idx) (h :: Bound) (Fin.FS (ibound (indexb idx))) (@boundi _ _ _ _ (indexb idx)) |}). Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2