proposition: Lemma beta_dec: forall M N, {M -b-> N} + {~ M -b-> N}.
proof: Proof. intros; unfold BetaReduction. apply red_dec. apply betaStep_dec. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)