It is well known that multiplicative linear logic (MLL) is conservative over intuitionistic multiplicative linear logic (IMLL). In other words, if an IMLL formula is provable in MLL then it is already provable in IMLL.
Who first proved this, and how? It doesn’t seem to be in Girard’s original Linear Logic paper, yet I've never seen a reference given when this fact is referred to.