∀ (p : DyckWord) (h : ¬p = 0),
  p.take (p.firstReturn + 1) ⋯ ≠ 0 ∧
    ∀ ⦃i : ℕ⦄,
      0 < i →
        i < (↑(p.take (p.firstReturn + 1) ⋯)).length →
          List.count DyckStep.D (List.take i ↑(p.take (p.firstReturn + 1) ⋯)) <
            List.count DyckStep.U (List.take i ↑(p.take (p.firstReturn + 1) ⋯))