proposition: Lemma Permutation_equiv `{!Equivalence (≡@{A})} l1 l2 l3 : l1 ≡ₚ l2 → l2 ≡ l3 → ∃ l2', l1 ≡ l2' ∧ l2' ≡ₚ l3.
proof: Proof. intros Hperm%symmetry Hequiv%symmetry. destruct (equiv_Permutation _ _ _ Hequiv Hperm) as (l2'&?&?). by exists l2'. Qed.
imports: stdpp(options)