Order-indiscernible sequence (source code)

= Order-indiscernible sequence

A sequence $(a_i)_{i\in I}$ indexed by a <total order> is order-indiscernible when any two increasing finite subsequences of the same length satisfy the same first-order formulas.