proposition: Lemma isFunApp_left : forall M (Mapp: isApp M), isFunApp M -> isFunApp (appBodyL Mapp).
proof: Proof. unfold isFunApp; intros. rewrite (appHead_app M Mapp) in H; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)