proposition: Lemma funS_head_subst : forall M G (MG: correct_subst M G), isFunS (appHead M) -> isFunS (appHead (subst MG)).
proof: Proof. destruct M as [E Pt A TypM]. simpl; induction TypM; try contr. intros; apply funS_is_funS with f. unfold subst; destruct (subst_aux MG) as [N [Nenv [Nterm Ntype]]]. term_inv N. intros. assert_app M_app (buildT (TApp TypM1 TypM2)). destruct (app_subst M_app MG) as [ML MR]. rewrite (appHead_app (subst MG) (app_subst_app M_app MG)). rewrite ML. apply IHTypM1. rewrite (appHead_app (buildT (TApp TypM1 TypM2)) M_app) in H; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)