Nella base principale per un termine M ci sono solo assunzioni relative alle variabili libere di M. Quando deriviamo un giudizio B |- M : tau B puo' contenere assunzioni anche per variabili che non sono in M. Quindi....