Occurrences under relation-symbol maps

Changing constraint symbols while retaining their scopes keeps the exact positive-CNF adapter and indexed occurrence list. Duplicate constraints remain separate positions. These original structural identities have no hypothesis about relation semantics.

theorem Cslib.Logic.PL.CSP.varCNF_mapRelation {Rel Other V : Type} (F : CSP Rel V) (f : Rel → Other) : varCNF (List.map (fun (x : Constraint Rel V) => match x with | (r, scope) => (f r, scope)) F) = F.varCNF

Relation-symbol maps retain the literal positive-clause adapter.

theorem Cslib.Logic.PL.CSP.occurrences_mapRelation {Rel Other V : Type} (F : CSP Rel V) (f : Rel → Other) : occurrences (List.map (fun (x : Constraint Rel V) => match x with | (r, scope) => (f r, scope)) F) = F.occurrences

Every indexed argument record stays unchanged under a relation-symbol map.