proposition: Lemma star_cons : forall t l t' l', star _ (one_step R) t' t -> star _ (one_step_list (one_step R)) l' l -> star _ (one_step_list (one_step R)) (t'::l') (t::l).
proof: Proof. intros t l t' l' H H0. apply star_trans with (t::l'). clear H0;induction H. constructor. apply star_trans with (y::l'). assumption. apply star_R;constructor;assumption. clear H;induction H0. constructor. apply star_trans with (t::y). assumption. apply star_R;constructor;assumption. Qed.
imports: CoLoR(weaved_relation closure terminaison) CoLoR(equational_theory_spec)