fact: Definition transl_message : forall (s : state) (im : message), (exists c : command, (exists sf : state, transition s c sf im)) -> {m : pmessage | transl_msg s im m}.
imports: Termes Conv Types Conv_Dec Infer Expr