Endpoint fibers in actual CSP incidence coordinates

Equality of incidence endpoints distinguishes the variable and constraint sides, then compares original variable labels or actual constraint positions. Repeated variables and constraints retain separate darts; dense vertex names do not require an injection on source labels.

theorem Cslib.Complexity.CSP.vertex_incidenceDart_eq_iff {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o p : F.Occurrence) (side other : Bool) : (incidenceDart o side).vertex = (incidenceDart p other).vertex ↔ side = other ∧ if side = true then o.fst = p.fst else o.var = p.var

Actual endpoint equality is exactly same side and the corresponding original label or constraint-position equality. This includes parallel occurrences and arbitrary source labels.