proposition: Theorem coherent_symmetric : forall (U:Type) (R:Relation U), Symmetric U (coherent U R).
proof: Proof. unfold coherent at 1. intros U R; red. intros x y H'; elim H'. intros z H'0; exists z; tauto. Qed.
imports: Relations_1 Relations_1_facts Relations_2 Relations_2_facts Relations_3