proposition: Lemma all_notin_singles_inv : forall xs ys vs, length ys = length vs -> xs ⊄ (ys ∷ vs) -> List.Forall (fun x => ¬ List.In x ys) xs.
proof: Proof. intros xs ys vs Heq Hnotin. unfold all_notin in Hnotin. elim (List.Forall_forall (fun x => ¬ In x ys) xs); intros Hyp1 Hyp2. apply Hyp2. intros x Hin. apply Hnotin in Hin. apply notin_singles_inv with vs; auto. Qed.
imports: Utf8 Equalities