proposition: Lemma Rstar_coherence : forall x y:A, star _ R x y -> coherence x y.
proof: Proof. intros x y H. apply coherence_intro with x. refine (star_refl _ _ _ ). exact H. Qed.
imports: CoLoR(weaved_relation closure terminaison)