Start of formal proof of MultiCompUnit