Relabeling back-and-forth equivalent tuples

BFEquiv.relabel: back-and-forth equivalence at any level is preserved under relabeling the index set by an arbitrary map σ : Fin m → Fin n (sub-tuples, repetitions, permutations), the back-and-forth analogue of SameAtomicType.relabel. The successor step extends σ to the new last coordinate (a private helper).

theorem FirstOrder.Language.BFEquiv.relabel {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (α : Ordinal.{u_1}) {n m : ℕ} {a : Fin n → M} {b : Fin n → N} : BFEquiv α n a b → ∀ (σ : Fin m → Fin n), BFEquiv α m (a ∘ σ) (b ∘ σ)

Relabeling: BFEquiv at every level is preserved by an arbitrary relabeling of the index set.