afn : Int -> Int -> Int
afn x y = ?arhs

-- plus_comm_rhs_1 : y = plus y 0
-- 
-- plus_comm : (x, y : Nat) -> plus x y = plus y x
-- plus_comm Z y = plus_comm_rhs_1
-- plus_comm (S k) y = ?plus_comm_rhs_2