proposition: Lemma horpo_abs_reduct : forall M (Mabs: isAbs M) N, M >> N -> exists Nabs: isAbs N, absBody Mabs >> absBody Nabs.
proof: Proof. intros. destruct H. destruct H3; try solve [term_inv M; try_solve | destruct H3; try_solve]. exists NAbs. constructor; trivial. term_inv M; term_inv N. term_inv M; term_inv N. apply algebraic_absBody; trivial. apply algebraic_absBody; trivial. rewrite (abs_proof_irr M Mabs MAbs); destruct H3; trivial. destruct (beta_abs_reduct Mabs H3); try_solve. exists x. apply beta_imp_horpo; try_solve. apply algebraic_absBody. hyp. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)