proposition: Lemma decide_typ : forall e t (tp : term), {typ e t tp} + {~ typ e t tp}.
proof: Proof. intros. elim decide_wf with e. intros wf_e. elim check_typ with e t tp; trivial. intros (err, expl_err, chk_err). right. apply chk_error_no_type with (1 := chk_err) (2 := expl_err). left; trivial. intros not_wf_e. right; red in |- *; intros. apply not_wf_e. apply typ_wf with (1 := H). Qed.
imports: Termes Conv Types Strong_Norm Conv_Dec