proposition: Theorem DisjointInv2 : forall (a : A) (L1 L2 : list A), Disjoint (a :: L1) L2 -> Disjoint L1 L2.
proof: Proof. intros a L1 L2 H'. apply DisjointCom. apply DisjointInv1 with (a := a); auto. apply DisjointCom; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)