Uniqueness of indexed literal occurrences

The proof follows the indexed-copy uniqueness argument in CNF.ThreeOccurrence.

Main results

• Cslib.Logic.PL.occurrences_nodup: clause and literal indices distinguish all occurrences.

theorem Cslib.Logic.PL.variable_mem_of_mem_occurrences {V : Type u_1} {φ : CNF V} {o : Occurrence V} (ho : o ∈ occurrences φ) : o.2.2.1 ∈ φ.vars

The variable named by an indexed literal occurrence occurs in the formula.

theorem Cslib.Logic.PL.occurrences_nodup {V : Type u_1} (φ : CNF V) : (occurrences φ).Nodup

Clause and literal indices distinguish every source occurrence, including repeated literals.