proposition: Lemma star_list : forall f l l', star _ (one_step_list (one_step R)) l' l -> star _ (one_step R) (Term f l') (Term f l).
proof: Proof. intros f l l' H. induction H. constructor. apply star_trans with (Term f y);auto. apply star_R. auto. constructor 2. auto. Qed.
imports: CoLoR(weaved_relation closure terminaison) CoLoR(equational_theory_spec)