let Ops = \(a : Type) -> \(r : Type) -> { ifNil : r, ifNode : a -> r -> r }

let InvList : Type -> Type
    = \(a : Type) -> forall (r : Type) -> Ops a r -> r

let example : InvList Integer
    = \(r : Type) ->
      \(op : Ops Integer r) ->
        op.ifNode +4 (op.ifNode +1 (op.ifNode +6 op.ifNil))

let length : forall (a : Type) -> InvList a -> Natural
    = \(a : Type) ->
      \(xs : InvList a) ->
        xs Natural { ifNil = 0, ifNode = \(_ : a) -> \(r : Natural) -> 1 + r }

in  length Integer example