proposition: Lemma betaStep_dec: forall M N, {BetaStep M N} + {~BetaStep M N}.
proof: Proof. intros. destruct (isApp_dec M) as [Mapp | Mnapp]. destruct (isAbs_dec (appBodyL Mapp)) as [MLabs | MLnabs]. destruct (eq_Term_dec N (lower (subst (beta_subst M Mapp MLabs)) (beta_lowering M Mapp MLabs))). left; rewrite e; constructor. right; intro MN; inversion MN. apply n; rewrite <- H0. apply term_eq. autorewrite with terms using trivial. autorewrite with terms using trivial. replace (absBody MLabs0) with (absBody MLabs). replace (appBodyR Mapp1) with (appBodyR Mapp); trivial. term_inv M. apply absBody_eq; term_inv M. right; intro MN; inversion MN. absurd (isAbs (appBodyL Mapp1)); trivial. replace (appBodyL Mapp1) with (appBodyL Mapp); trivial. term_inv M. right; intro MN; inversion MN; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)