improve notation of theorem-1 using local bindings