proposition: Lemma arg_subterm : forall M Ma, isArg Ma M -> subterm Ma M.
proof: Proof. unfold isArg, appArgs. intros. destruct (isApp_dec M). apply appUnit_subterm; trivial. unfold isAppUnit; auto with datatypes. rewrite appUnits_notApp in H; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)