PowerWebster_ILL Intuitionistic Linear Logic in Coq (from Power and Webtser TPHOL 1999) From source files.