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