functor (E : TraceChecker.S-> TraceChecker.S