proposition: Lemma chk_error_no_type : forall e (m : term) t (err : type_error), chk_error m t err -> expln e err -> ~ typ e m t.
proof: Proof. simple destruct 1; intros. apply inf_error_no_type with err0; auto with coc arith. red in |- *; intros. elim type_case with e m t; intros; auto with coc arith. inversion_clear H4. elim inf_error_no_type with t err0 e (Srt x); auto with coc arith. inversion_clear H0; auto with coc arith. Qed.
imports: Termes Conv Types Strong_Norm Conv_Dec