proposition: Lemma horpo_comp_abs : forall M (Mabs: isAbs M), algebraic M -> (forall G (cs: correct_subst (absBody Mabs) G) T, isSingletonSubst T G -> CompH T -> CompH (subst cs)) -> CompH M.
proof: Proof. intros M Mnorm Mabs H; unfold CompH. eapply comp_abs; eauto with horpo. Qed.
imports: CoLoR(RelExtras ListExtras Computability Horpo) Coq(Setoid Morphisms)