proposition: Lemma horpo_comp_pflat N Ns : isPartialFlattening Ns N -> algebraic N -> AllComputable horpo Ns -> CompH N.
proof: Proof. intros NsN Nnorm NsC; unfold CompH. apply comp_pflat with Ns; trivial. Qed.
imports: CoLoR(RelExtras ListExtras Computability Horpo) Coq(Setoid Morphisms)