proposition: Theorem NoDup_app_l : forall (A : Type)(ls1 ls2 : list A), NoDup (ls1 ++ ls2) -> NoDup ls1.
proof: Proof. intuition. eapply NoDup_app in H. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation