proposition: Lemma app_subst_app (M: Term) (Mapp: isApp M) G (CS: correct_subst M G) : isApp (subst CS).
proof: Proof. term_inv M. unfold subst; destruct (subst_aux CS) as [T [Tenv [Tterm Ttype]]]. unfold presubst in Tterm; simpl in *. eapply app_isApp; eauto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)