proposition: Lemma trans_error_no_confusion : forall (si sf : state) (c : command) (m : message) (err : error), transition si c sf m -> com_error si c err -> False.
proof: Proof. simple induction 1; intros. inversion_clear H1. elim inf_error_no_type with m0 err0 (glob_ctx si) t; auto with coc core arith datatypes. inversion_clear H1. elim chk_error_no_type with (glob_ctx si) m0 t err0; auto with coc core arith datatypes. inversion_clear H2. elim decl_err_not_wf with (glob_ctx si) t err0; auto with coc core arith datatypes. elim H0. apply glob_wf_ctx. cut (exists n : nat, item _ x (glob_names si) n); intros. inversion_clear H2. absurd (0 = S x0); auto with coc core arith datatypes. generalize (glob_unique s2). unfold name_unique in |- *; intros. apply H2 with x. rewrite H1; auto with coc core arith datatypes. rewrite H1; auto with coc core arith datatypes. elim H3; intros. split with 0; auto with coc core arith datatypes. inversion_clear H4. split with (S x0); auto with coc core arith datatypes. inversion_clear H1. rewrite H2 in H0. discriminate H0. inversion_clear H0. inversion_clear H0. Qed.
imports: Termes Conv Types Conv_Dec Infer Expr