fact: Definition com_answer (si : state) (c : command) : Set := ({p : state * message | match p with | (sf, m) => transition si c sf m end} + {e : error | com_error si c e})%type.
imports: Termes Conv Types Conv_Dec Infer Expr