proposition: Lemma subst_appR_c M (Mapp: isApp M) G : correct_subst M G -> correct_subst (appBodyR Mapp) G.
proof: Proof. term_inv M. fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)