proposition: Lemma firstn_eq_all_gen : forall (A : Type)(ls : list A) n, n = length ls -> firstn n ls = ls.
proof: Proof. induction ls; intuition; subst; simpl in *. trivial. f_equal. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation