proposition: Lemma appBodyL_term : forall M PtL PtR (Mterm: term M = PtL @@ PtR) (Mapp: isApp M), term (appBodyL Mapp) = PtL.
proof: Proof. intros; term_inv M. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)