Permutation invariance from binary symmetry

List.Perm.congr_arity₂: a list function symmetric on pairs and constant above length two is Perm-invariant. Keystone for node algebras whose only order-sensitive shape is binary (Merge-style algebras over unordered daughters).

theorem List.Perm.congr_arity₂ {β : Type u_1} {γ : Type u_2} {g : List β → γ} {c : γ} (hswap : ∀ (x y : β), g [x, y] = g [y, x]) (hbig : ∀ (l : List β), 2 < l.length → g l = c) {l₁ l₂ : List β} (h : l₁.Perm l₂) : g l₁ = g l₂

A list function symmetric on pairs and constant above length two is Perm-invariant: lengths ≤ 1 are rigid under permutation, pairs by the symmetry, longer lists by the constancy.