proposition: Lemma listRepeat_length : forall n (A : Type) (a : A), length (listRepeat a n) = n.
proof: Proof. induction n; intuition; simpl in *. f_equal. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation