proposition: Lemma decl_err_not_wf : forall e t (err : type_error), decl_error t err -> expln e err -> ~ wf (t :: e).
proof: Proof. red in |- *. simple destruct 1; intros. inversion_clear H2. elim inf_error_no_type with t err0 e (Srt s); auto with coc arith. inversion_clear H0. inversion_clear H1. elim H3 with s; auto with coc arith. Qed.
imports: Termes Conv Types Strong_Norm Conv_Dec