proposition: Lemma replicate_as_elem_of x n l : replicate n x = l ↔ length l = n ∧ ∀ y, y ∈ l → y = x.
proof: Proof. split; [intros <-; eauto using elem_of_replicate_inv, replicate_length|]. intros [<- Hl]. symmetry. induction l as [|y l IH]; f_equal/=. - apply Hl. by left. - apply IH. intros ??. apply Hl. by right. Qed.
imports: stdpp(options)