proposition: Lemma in_listRepeat_inv : forall n (A : Type)(a1 a2 : A), In a1 (listRepeat a2 n) -> a1 = a2.
proof: Proof. induction n; intuition; simpl in *. intuition. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation