proposition: Lemma type_appBodyL_subst M G (MG: correct_subst M G) (Mapp: isApp M) (MGapp: isApp (subst MG) := app_subst_app Mapp MG) : type (appBodyL Mapp) = type (appBodyL MGapp).
proof: Proof. destruct (app_subst Mapp MG). unfold MGapp; rewrite H. autorewrite with terms; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)