proposition: Lemma base_step_base : forall M N, isBaseType (type M) -> M -R-> N -> isBaseType (type N).
proof: Proof. intros M N Mbase MN. rewrite <- (R_type_preserving MN); trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)