proposition: Lemma to_list_In_eq : forall {A} (t: array A) i x, i <? length t = true -> x = t.[i] -> In x (to_list t).
proof: Proof. intros A t i x Hi ->. now apply to_list_In. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz