proposition: Lemma algebraic_appUnits : forall M, algebraic M -> ~isFunApp M -> forall M', isAppUnit M' M -> algebraic M'.
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => algebraic M -> ~isFunApp M -> forall M', isAppUnit M' M -> algebraic M'). apply subterm_wf. clear M; intros M IH Malg Mnfa M' M'M. destruct (isApp_dec M) as [Mapp | Mnapp]. destruct (appUnit_app M' M Mapp M'M). rewrite H. apply algebraic_appBodyR; trivial. apply IH with (appBodyL Mapp); trivial. apply appBodyL_subterm. apply algebraic_appBodyL; trivial. apply notFunApp_left_inv; trivial. unfold isAppUnit in M'M. rewrite (appUnits_notApp M Mnapp) in M'M. inversion M'M; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)