proposition: Lemma argsComp_appComp : forall M, algebraic M -> isFunS (appHead M) -> (forall P, isArg P M -> CompH P) -> CompH M.
proof: Proof. intros M Mnorm Mhead argsComp. set (Args := @exist _ (fun Ts: Terms => CompTerms Ts) _ argsComp). assert (Mf: exists f, term (appHead M) = ^f). set (MH := appHead M) in *. term_inv MH. exists f; trivial. destruct Mf as [f Mhead_f]. apply argsComp_appComp_ind with (P := (f, Args))(M := M); trivial. Qed.
imports: CoLoR(RelExtras ListExtras Horpo Computability PairLex HorpoComp LogicUtil)