fact: Definition answer (si : state) (a : ast) : Set := ({p : state * pmessage | match p with | (sf, m) => top_trans si a sf m end} + {err : perror | top_error si a err})%type.
imports: Termes Conv Types Conv_Dec Infer Expr