proposition: Theorem DisjointCons2 : forall (a : A) (L1 L2 : list A), Disjoint L1 L2 -> ~ InEq a L2 -> Disjoint (a :: L1) L2.
proof: Proof. intros a L1 L2 H' H'0; apply DisjointCom; auto. apply DisjointCons1; auto. apply DisjointCom; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)