proposition: Theorem DisjointInclL : forall L1 L2 L3 : list A, Disjoint L1 L2 -> InclEq L3 L1 -> Disjoint L3 L2.
proof: Proof. intros L1 L2 L3 H' H'0. apply DisjointDef; auto. intros a H'1; inversion H'. apply H; auto. inversion H'0; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)