proposition: Lemma firstn_app_eq : forall (A : Set)(ls1 ls2 : list A), firstn (length ls1) (ls1 ++ ls2) = ls1.
proof: Proof. induction ls1; intuition; simpl in *. f_equal. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation