proposition: Lemma horpo_comp_lift : forall N, CompH N -> CompH (lift N 1).
proof: Proof. intros. setoid_replace (lift N 1) with N using relation terms_conv; trivial. apply terms_conv_sym; apply terms_lift_conv. Qed.
imports: CoLoR(RelExtras ListExtras Computability Horpo) Coq(Setoid Morphisms)