Literal edge positions of appended-scope occurrences

An appended argument occupies the old occurrence count plus its original argument position. The formula is independent of repeated variable labels and duplicate constraint tuples. This original coordinate identity uses the existing actual occurrence type and incidence edge list.

theorem Cslib.Complexity.CSP.incidenceEdgeIndex_appendOfFnOccurrenceEquiv_inr {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (j : Fin n) : incidenceEdgeIndex ((F.appendOfFnOccurrenceEquiv r scope) (Sum.inr j)) = F.occurrences.length + ↑j

The appended argument's incidence edge is the body-prefix length plus its actual slot. The empty-scope case has no argument to select. Variable names need not be distinct.