proposition: Lemma In_to_list : forall {A} (t: array A) x, In x (to_list t) -> exists i, i <? length t = true /\ x = t.[i].
proof: Proof. intros A t x; assert (Bt := to_Z_bounded (length t)); unfold to_list. rewrite <- in_rev. set (a := foldi _ _ _ _); pattern (length t) at 0, a; subst a; apply foldi_ind. rewrite leb_spec, to_Z_0; lia. intro H; elim (in_nil H). intros i a _; assert (Bi := to_Z_bounded i); rewrite ltb_spec; intros Hi IH. intro Hin; case (in_inv Hin); clear Hin; [ | exact IH ]. intro H; rewrite <- H; clear H. exists i. split; [ rewrite ltb_spec; lia | reflexivity ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz