proposition: Lemma horpo_comp_app : forall M (Mapp: isApp M), CompH (appBodyL Mapp) -> CompH (appBodyR Mapp) -> CompH M.
proof: Proof. intros M Mapp Ml Mr; unfold CompH. apply comp_app with Mapp; trivial. Qed.
imports: CoLoR(RelExtras ListExtras Computability Horpo) Coq(Setoid Morphisms)