proposition: Theorem diffElemNone : forall L1 L2 : list A, diffElem L1 L2 = None -> InclEq L1 L2.
proof: Proof. intros L1; elim L1; simpl in |- *; auto. intros a l H' L2. case (InEqDec a L2); auto. intros H'0 H'1; discriminate. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)