proposition: Lemma beta_abs_reduct : forall M (Mabs: isAbs M) N, M -b-> N -> exists Nabs: isAbs N, absBody Mabs -b-> absBody Nabs.
proof: Proof. intros M Mabs N MN. inversion MN; term_inv M; try_solve. inversion H; try_solve. exists Nabs; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)