proposition: Lemma base_comp_step_comp : forall M N, isBaseType (type M) -> Computable M -> M -R-> N -> Computable N.
proof: Proof. intros M N Mbase Mcomp MN. apply CompBasic. apply base_step_base with M; trivial. apply R_algebraic_preserving with M; trivial. apply comp_algebraic; trivial. unfold AccR; apply Acc_inv with M; auto. apply CompCaseBasic; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)