proposition: Lemma funS_headS_subst : forall M f G (MG: correct_subst M G), term (appHead M) = ^f -> term (appHead (subst MG)) = ^f.
proof: Proof. destruct M as [E Pt A TypM]. induction TypM; try_solve; intros. autorewrite with terms using unfold presubst; trivial. assert (isFunS (subst MG)). apply funS_is_funS with f. rewrite funS_presubst; simpl; trivial. term_inv (subst MG). destruct (app_subst (M:=buildT (TApp TypM1 TypM2)) I MG). set (MG_app := app_subst_app (M:=buildT (TApp TypM1 TypM2)) I MG). rewrite (appHead_app (subst MG) MG_app). unfold MG_app; rewrite H0. apply IHTypM1; trivial. rewrite (appHead_app (buildT (TApp TypM1 TypM2)) I) in H; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)