proposition: Lemma inf_error_no_type : forall (m : term) (err : type_error), inf_error m err -> forall e, expln e err -> forall t, ~ typ e m t.
proof: Proof. simple induction 1; intros. inversion_clear H0; red in |- *; intros. apply inv_typ_abs with e m0 n0 t; intros; auto with coc arith. elim H2 with e (Srt s1); auto with coc arith. apply inv_typ_app with e m0 v t; intros; auto with coc arith. elim H2 with e (Prod V Ur); auto with coc arith. apply inv_typ_app with e u m0 t; intros; auto with coc arith. elim H2 with e V; auto with coc arith. apply inv_typ_prod with e m0 n0 t; intros; auto with coc arith. elim H2 with e (Srt s1); auto with coc arith. inversion_clear H3. inversion_clear H0; red in |- *; intros. apply inv_typ_abs with e T m0 t; intros; auto with coc arith. elim H2 with (T :: e) T0; auto with coc arith. apply inv_typ_prod with e T m0 t; intros; auto with coc arith. elim H2 with (T :: e) (Srt s2); auto with coc arith. inversion_clear H0; auto with coc arith. red in |- *; intros. apply inv_typ_ref with e t n; intros; auto with coc arith. inversion_clear H0. generalize H5. elim H2; simpl in |- *; intros; auto with coc arith. inversion_clear H0. inversion_clear H0. red in |- *; intros. apply inv_typ_abs with e T M t; intros; auto with coc arith. elim inv_typ_conv_kind with (T :: e) T0 (Srt s2); auto with coc arith. apply typ_unique with (T :: e) M; auto with coc arith. inversion_clear H0. red in |- *; intros. apply inv_typ_abs with e m0 n t0; intros; auto with coc arith. elim H2 with s1; auto with coc arith. inversion_clear H0. red in |- *; intros. apply inv_typ_app with e m0 n t0; intros; auto with coc arith. elim H2 with V Ur; auto with coc arith. inversion_clear H0. red in |- *; intros. apply inv_typ_app with e m0 n t; intros; auto with coc arith. elim type_case with e m0 (Prod a b); intros; auto with coc arith. inversion_clear H7. apply inv_typ_prod with e a b (Srt x); intros; auto with coc arith. apply H3. apply type_conv with V s1; auto with coc arith. apply inv_conv_prod_l with Ur b. apply typ_unique with e m0; auto with coc arith. discriminate H7. inversion_clear H0. red in |- *; intros. apply inv_typ_prod with e m0 n t0; intros; auto with coc arith. elim H2 with s1; auto with coc arith. inversion_clear H0. inversion_clear H1. red in |- *; intros. apply inv_typ_prod with e m0 n t0; intros; auto with coc arith. elim H2 with s2; auto with coc arith. Qed.
imports: Termes Conv Types Strong_Norm Conv_Dec