proposition: Lemma horpo_comp_units_comp M : (forall N, isAppUnit N M -> CompH N) -> CompH M.
proof: Proof. intro Munits; unfold CompH. apply comp_units_comp; trivial. Qed.
imports: CoLoR(RelExtras ListExtras Computability Horpo) Coq(Setoid Morphisms)