proposition: Lemma not_In_app : forall (A : Type) (xs ys : list A) (x : A), ~ In x xs -> ~ In x ys -> ~ In x (xs ++ ys).
proof: Proof. intros ? xs ys x ? ? H. apply in_app_or in H. intuition. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac