proposition: Lemma app_beta_funS : forall M N, isFunS (appHead M) -> M -b-> N -> isFunS (appHead N).
proof: Proof. intros. destruct (funS_fun (appHead M) H) as [f Mf]. apply funS_is_funS with f. apply (app_beta_headSymbol H0 Mf). Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)