Remove NF conditions from the rules

[eyihluyc]

This PR removes NF conditions from the rule set.

Also, test from #448 is fixed, but the issue still needs to be considered, because this breaks confluence.

The confluence via Quickcheck fails as well, but not because of the above; there are critical pairs with ⊥ that do not look critical to me, e.g.:

Source term:
⟦ 
  φ ↦ ⟦
    x8 ↦ ⊥.v4, 
    φ ↦ ⟦ ⟧
  ⟧.φ
⟧
Critical pair:
  Using rule 'R_DOT': 
  ⟦
    φ ↦ ⟦ 
      ρ ↦ ⟦
        φ ↦ ⟦ ⟧,
        x8 ↦ ⊥.v4
      ⟧
    ⟧
  ⟧

  Using rule 'R_DD': 
  ⟦
    φ ↦ ⟦
      x8 ↦ ⊥, 
      φ ↦ ⟦ ⟧
    ⟧.φ
  ⟧

---

PR-Codex overview

This PR focuses on updating object structures and fixing application patterns related to ξ in the codebase.

Detailed summary

• Updated object structures in dataization.yaml
• Fixed application patterns involving ξ in dataization.yaml
• Modified context and patterns for rules in yegor.yaml

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}

[fizruk]

I think this is because we explicitly avoid applying any rules under $\rho$-bindings:

https://github.com/objectionary/normalizer/blob/a262f572f779a4040da79478207f4990523d5a3d/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs#L145-L147

I believe this exists for two reasons:

1. Previously, we forced everything to NF, so we should not have any not-normalized terms as $\rho$.
2. Computing inside $\rho$ is generally redundant, and may lead to explosion of the term. This is, however, not relevant in the context of confluence test as far as I can see. So we can allow reduction under $\rho$ for confluence tests, but forbid them when actually normalizing stuff (making it more lazy in a sense).