proposition: Lemma term_appBodyL_eq : forall M N (Mapp: isApp M) (Napp: isApp N), term M = term N -> term (appBodyL Mapp) = term (appBodyL Napp).
proof: Proof. intros M N; term_inv M; term_inv N. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)