proposition: Lemma subst_list_args : forall M G (MG: correct_subst M G), isFunS (appHead M) -> subst_list (appArgs M) (appArgs (subst MG)) G.
proof: Proof. intros. unfold appArgs, subst_list. apply list_sim_tail. apply subst_list_units; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)