foo : Nat -> Nat -> Nat foo k j = ?foo_rhs1