proposition: Lemma top_trans_error_no_confusion : forall (si sf : state) (a : ast) (m : pmessage) (perr : perror), top_trans si a sf m -> top_error si a perr -> False.
proof: Proof. simple induction 1; intros. inversion_clear H3. apply synth_no_confusion with si a c perr; auto with coc core arith datatypes. apply trans_error_no_confusion with si sf c im ie; auto with coc core arith datatypes. elim synth_deterministic with si a c0 c; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Conv_Dec Infer Expr