proposition: Lemma comp_lift_comp M n : Computable M -> Computable (lift M n).
proof: Proof. intro. rewrite <- (terms_lift_conv M n); trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)