proposition: Lemma appArg_left : forall M N (Mapp: isApp M), isArg N (appBodyL Mapp) -> isArg N M.
proof: Proof. intros M N Mapp Narg. unfold isArg in *. rewrite (appArgs_app M Mapp). auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)