proposition: Lemma decide_wf : forall e, {wf e} + {~ wf e}.
proof: Proof. simple induction e; intros. left. apply wf_nil. elim H. intros wf_l. elim add_typ with l a; trivial. intros (err, expl_err, decl_err). right. apply decl_err_not_wf with (1 := decl_err) (2 := expl_err). left; trivial. intros not_wf_l. right; red in |- *; intros. apply not_wf_l. inversion_clear H0. apply typ_wf with (1 := H1). Qed.
imports: Termes Conv Types Strong_Norm Conv_Dec