proposition: Lemma replicate_Permutation n x l : replicate n x ≡ₚ l → replicate n x = l.
proof: Proof. intros Hl. apply replicate_as_elem_of. split. - by rewrite <-Hl, replicate_length. - intros y. rewrite <-Hl. by apply elem_of_replicate_inv. Qed.
imports: stdpp(options)