proposition: Lemma Computable_morph_aux : forall x1 x2 : Term, x1 ~ x2 -> (Computable x1 -> Computable x2).
proof: Proof. intro M. term_type_inv M; intros M' MM' Mcomp. apply CompBasic. rewrite <- (terms_conv_eq_type MM'); try_solve. rewrite <- MM'; apply comp_algebraic; trivial. rewrite <- MM'. apply CompCaseBasic; simpl; trivial. apply CompArrow. rewrite <- MM'; apply comp_algebraic; trivial. rewrite <- (terms_conv_eq_type MM'); try_solve. intros N Napp Nnorm NR NL. apply (CompCaseArrow Mcomp I N Napp NR NL). apply terms_conv_trans with M'; auto with terms_eq. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)