example no.12 doesn't rewrite correctly

[yegor256]

I'm doing this:

$ cat >bar.phi
{⟦ m ↦ ⟦ x ↦ ⟦ t ↦ ∅ ⟧ (t ↦ ξ.k), k ↦ ⟦ λ ⤍ Fn ⟧ ⟧.x.t.p ⟧}
$ eo-phi-normalizer rewrite -s --max-depth 15 bar.phi
{
  ⟦
    m ↦ ⟦
      t ↦ ∅
    ⟧
    (
      t ↦ ⟦
        x ↦ ⟦
          t ↦ ⟦
            x ↦ ⟦
              t ↦ ⟦
                x ↦ ⟦
                  t ↦ ⟦
                    x ↦ ⟦
                      t ↦ ⟦
                        x ↦ ⟦
                          t ↦ ⟦
                            x ↦ ⟦
                              t ↦ ⟦
                                x ↦ ⟦
                                  t ↦ ⟦
                                    x ↦ ⟦
                                      t ↦ ∅
                                    ⟧
                                    (
                                      t ↦ ξ.k
                                    ),
                                    k ↦ ⟦
                                      λ ⤍ Fn
                                    ⟧
                                  ⟧
                                  .k
                                ⟧,
                                k ↦ ⟦
                                  λ ⤍ Fn
                                ⟧
                              ⟧
                              .k
                            ⟧,
                            k ↦ ⟦
                              λ ⤍ Fn
                            ⟧
                          ⟧
                          .k
                        ⟧,
                        k ↦ ⟦
                          λ ⤍ Fn
                        ⟧
                      ⟧
                      .k
                    ⟧,
                    k ↦ ⟦
                      λ ⤍ Fn
                    ⟧
                  ⟧
                  .k
                ⟧,
                k ↦ ⟦
                  λ ⤍ Fn
                ⟧
              ⟧
              .k
            ⟧,
            k ↦ ⟦
              λ ⤍ Fn
            ⟧
          ⟧
          .k
        ⟧,
        k ↦ ⟦
          λ ⤍ Fn
        ⟧
      ⟧
      .k
    )
    (
      ρ ↦ ⟦
        x ↦ ⟦
          t ↦ ∅
        ⟧
        (
          t ↦ ξ.k
        ),
        k ↦ ⟦
          λ ⤍ Fn
        ⟧
      ⟧
    )
    .t.p
  ⟧
}

This is not the result expected. I expect to get this instead:

{⟦ m ↦ ⟦ λ ⤍ Fn, ρ ↦ ⟦ x ↦ ⟦ t ↦ ∅ ⟧ (t ↦ ξ.k), k ↦ ⟦ λ ⤍ Fn ⟧ ⟧ ⟧.p ⟧}