proposition: Lemma red_dec : forall M N, {Red M N} + {~Red M N}.
proof: Proof. intro M. apply well_founded_induction_type with (R := subterm) (P := fun M => forall N, {Red M N} + {~Red M N}). apply subterm_wf. clear M; intros M IH N. destruct (step_dec M N). left; apply RedStep; trivial. destruct (isApp_dec M) as [Mapp | Mnapp]. destruct (isApp_dec N) as [Napp | Nnapp]. destruct (IH (appBodyL Mapp) (appBodyL_subterm M Mapp) (appBodyL Napp)). destruct (eq_Term_dec (appBodyR Mapp) (appBodyR Napp)). left; apply RedAppL with Mapp Napp; trivial. destruct (IH (appBodyR Mapp) (appBodyR_subterm M Mapp) (appBodyR Napp)). destruct (eq_Term_dec (appBodyL Mapp) (appBodyL Napp)). left; apply RedAppR with Mapp Napp; trivial. right; intro MN; inversion MN; try_solve. apply n0; term_inv M; term_inv N. apply n1; term_inv M; term_inv N. term_inv M. right; intro MN; inversion MN; try_solve. apply n0; term_inv M; term_inv N. apply n1; term_inv M; term_inv N. term_inv M. destruct (IH (appBodyR Mapp) (appBodyR_subterm M Mapp) (appBodyR Napp)). destruct (eq_Term_dec (appBodyL Mapp) (appBodyL Napp)). left; apply RedAppR with Mapp Napp; trivial. right; intro MN; inversion MN; try_solve. apply n0; term_inv M; term_inv N. apply n1; term_inv M; term_inv N. term_inv M. right; intro MN; inversion MN; try_solve. apply n0; term_inv M; term_inv N. apply n1; term_inv M; term_inv N. term_inv M. right; intro MN; inversion MN; try_solve. term_inv M. destruct (isAbs_dec M) as [Mabs | Mnabs]. destruct (isAbs_dec N) as [Nabs | Nnabs]. destruct (IH (absBody Mabs) (absBody_subterm M Mabs) (absBody Nabs)). destruct (eq_SimpleType_dec (absType Mabs) (absType Nabs)). left; apply RedAbs with Mabs Nabs; trivial. right; intro MN; inversion MN; try_solve. apply n0; term_inv M; term_inv N. right; intro MN; inversion MN; try_solve. apply n0; term_inv M; term_inv N. right; intro MN; inversion MN; try_solve. right; intro MN; inversion MN; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubstConv)