--#include "SPS.alfa"
--#include "../SPSProofs.alfa"
proof :: Module_SPS.Separation1 = proofSeparation1