proposition: Lemma Forall_eq_repeat x l : Forall (eq x) l -> l = repeat x (length l).
proof: Proof. induction l as [|a l IHl]; simpl; intros HF; auto. inversion_clear HF as [ | ? ? ? HF']; subst. now rewrite (IHl HF') at 1. Qed.
imports: PeanoNat