proposition: Lemma rwr_as_star : forall R t t', Eqt.rwr R t t' -> star _ (Eqt.one_step R) t t'.
proof: Proof. induction 1. apply star_R. assumption. apply star_trans with y;auto. right with x; [left | assumption]. Qed.
imports: Coq(List Bool FunInd) CoLoR(weaved_relation closure term_spec terminaison)