proposition: Lemma betaStep_algebraic_preserving : forall M N, algebraic M -> BetaStep M N -> algebraic N.
proof: Proof. intros. inversion H0. apply algebraic_lower. apply algebraic_subst. apply algebraic_absBody. apply algebraic_appBodyL; trivial. unfold isFunApp in * . assert (isAbs (appHead M)). rewrite (appHead_app M Mapp0). rewrite (appHead_notApp (appBodyL Mapp0)); trivial. apply abs_isnot_app; trivial. term_inv (appHead M). apply singletonSubst_algebraic with (lift (appBodyR Mapp0) 1). apply singletonSubst_cond. apply algebraic_lift. apply algebraic_appBodyR; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)