proposition: Lemma prop_rel_sym A B (f : A -> B -> Prop) R S : Symmetric R -> Symmetric S -> Proper (R ==> S ==> impl) f -> Proper (R ==> S ==> iff) f.
proof: Proof. intros R_sym S_sym f_prop x x' xx' y y' yy'. split; intro h. eapply f_prop. apply xx'. apply yy'. hyp. eapply f_prop. sym. apply xx'. sym. apply yy'. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)