Adjacent identification on actual ordered boundary words

The first two distinct boundary labels supply cofacial corners through consecutive actual probe arguments. Their precise selected-pair kernel is imposed on the actual body and boundary labels. The first duplicate marker is deleted, retaining the survivor order. No boundary label needs an occurrence in the unaugmented body.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.Witness.identifyFirstTwoOfFn {Rel V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {n : ℕ} {v : Fin (n + 2) → V} (w : Witness F (List.ofFn v)) (f : V → W) (hv : v 0 ≠ v 1) (hk : ∀ a ∈ F.vars ++ List.ofFn v, ∀ b ∈ F.vars ++ List.ofFn v, f a = f b ↔ Function.update id (v 1) (v 0) a = Function.update id (v 1) (v 0) b) (hn : (List.ofFn fun (i : Fin (n + 1)) => f (v i.succ)).Nodup) : Witness (Logic.PL.CSP.relabel f F) (List.ofFn fun (i : Fin (n + 1)) => f (v i.succ))

Identify the first two boundary labels and remove the first marker. The actual body is exactly relabeled by f; the target boundary is precisely the mapped source tail.