Appending an argument to the last indexed constraint

The actual ordered occurrence list gains one final record, retaining every previous constraint/scope position even with repeated variables or identical constraints. This original list identity is independent of incidence graphs and relation semantics.

theorem Cslib.Logic.PL.CSP.occurrences_append_last_argument {Rel V : Type} (F : CSP Rel V) (r : Rel) (scope : List V) (v : V) : (F ++ [(r, scope ++ [v])]).occurrences = (F ++ [(r, scope)]).occurrences ++ [(List.length F, scope.length, v)]

Appending one argument to the last constraint appends exactly one occurrence record. Repeated variables and identical constraints remain indexed rather than deduplicated.