proposition: Lemma CompH_morph_aux : forall x1 x2 : Term, x1 ~ x2 -> CompH x1 -> CompH x2.
proof: Proof. intros t t' teqt' H_t. unfold CompH. apply Computable_morph_aux with t; eauto with horpo. Qed.
imports: CoLoR(RelExtras ListExtras Computability Horpo) Coq(Setoid Morphisms)