proposition: Lemma SetoidPermutation_stronger {A} (R U: relation A): (forall x y: A, R x y → U x y) → forall a b, SetoidPermutation R a b → SetoidPermutation U a b.
proof: Proof. intros ??? P. induction P; eauto. Qed.
imports: Coq.Unicode.Utf8 Coq.Setoids.Setoid CoRN.stdlib_omissions.List Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms