The block odd list, order-exactly

The odd list of a block of the flipped data colouring is the Definition 5 value map over the block-slot flag enumeration, entry by entry.

theorem RS.oddListOf_blockRestrict_eq_map {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) : oddListOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v) = List.map (defFiveValue o φ) (blockOddFlagList W F v)

The block odd list is the value map of the block enumeration (order-exact).