proposition: Lemma algebraic_arg : forall M Marg (Mapp: isApp M), algebraic M -> isArg Marg M -> algebraic Marg.
proof: Proof. intros; destruct (isApp_dec M); try_solve. inversion H; term_inv M. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)