:: deftheorem defines tail FOMODEL2:def 37 :
for S being Language
for phi being wff string of S holds tail phi = (SubWffsOf phi) `2 ;