% TOADD 4

To avoid notational cluttering in relevant lambda terms it is 
possible to unsugar the basic system, \ie have only atoms, relevant 
arrow and exponentials and defining intuitionistic implication as 
usual $\A\Imp B=_{def} (!A) \RImp B$. This rules out two abstractions 
and two application symbols. Too bad this bang calculus does not have 
unicity of canonical forms. Indeed, as for or-elimination, bang 
elimination is an indirect rules which brings in \emph{commutative} 
reductions. While (strong) normalization and the subfomula principle 
are attainable, we end up dealing with equivalence classes of 
canonical forms. The situation may be manageable as far as the 
implicational-bang fragment is concerned, but it is bound to get 
unwieldy for larger fragments.