proposition: Lemma reverse_replicate n x : reverse (replicate n x) = replicate n x.
proof: Proof. symmetry. apply replicate_as_elem_of. rewrite reverse_length, replicate_length. split; auto. intros y. rewrite elem_of_reverse. by apply elem_of_replicate_inv. Qed.
imports: stdpp(options)