proposition: Theorem coherent_symmetric : forall (U : Type) (R : Relation U), Symmetric (coherent R).
proof: Proof. unfold coherent at 1 in |- *. intros U R; red in |- *. intros x y h; elim h; intros z h0; elim h0; intros H' H'0; clear h h0. exists z; auto. Qed.
imports: Relations Confluence