proposition: Lemma appArg_app : forall M Marg, isArg Marg M -> isApp M.
proof: Proof. intro M. destruct (isApp_dec M); trivial. unfold isArg; rewrite appArgs_notApp; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)