Wasn’t this idea the basic premise of coq? Why didn’t it work?