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