proposition: Lemma app_typeL_type : forall M A B (Mapp: isApp M), type (appBodyL Mapp) = A --> B -> type M = B.
proof: Proof. intros M A B Mapp Ml. term_inv M. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)