proposition: Theorem Rstar_imp_coherent : forall (U:Type) (R:Relation U) (x y:U), Rstar U R x y -> coherent U R x y.
proof: Proof. intros U R x y H'; red. exists y; auto with sets. Qed.
imports: Relations_1 Relations_1_facts Relations_2 Relations_2_facts Relations_3