Extensionality in actual occurrence positions

The two original constraint and argument indices identify an occurrence; its variable is read from the original scope. No variable-label equality or injectivity premise is needed.

theorem Cslib.Logic.PL.CSP.Occurrence.eq_of_positions {Rel V : Type} {F : CSP Rel V} {o p : F.Occurrence} (hc : ↑o.fst = ↑p.fst) (ha : ↑o.snd = ↑p.snd) : o = p

Constraint and argument position values determine an actual dependent occurrence.