proposition: Theorem DisjointCom : forall L1 L2 : list A, Disjoint L1 L2 -> Disjoint L2 L1.
proof: Proof. intros L1 L2 H'; elim H'; auto. intros L3 L4 H'0. apply DisjointDef. intros a H'1; red in |- *; intros H'2; absurd (InEq a L4); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)