Plugging-in proof development environments using Locks in LF