recursion.dhall

let Rule
    : Type
    = ∀(_Rule : Type) →
      ∀(One : _Rule) →
      ∀(Two : _Rule) →
      ∀(Many : List _Rule → _Rule) →
        _Rule

let example
    : Rule
    = λ(_Rule : Type) →
      λ(One : _Rule) →
      λ(Two : _Rule) →
      λ(Many : List _Rule → _Rule) →
        Many [ One, Two, Many [ Two, One ] ]

let all
    : Rule → Natural
    = λ(r : Rule) →
        r
          Natural
          1
          2
          ( λ(many : List Natural) →
              List/fold
                Natural
                many
                Natural
                (λ(x : Natural) → λ(y : Natural) → x + y)
                0
          )

in  all example