proposition: Lemma comp_app : forall M (Mapp: isApp M), Computable (appBodyL Mapp) -> Computable (appBodyR Mapp) -> Computable M.
proof: Proof. intros M; term_inv M. intros TrApp T1c T2c. apply CompCaseArrow with (buildT T1) I; auto with terms_eq. apply comp_algebraic; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)