proposition: Theorem DisjointCons1 : forall (b : A) (L1 L2 : list A), Disjoint L1 L2 -> ~ InEq b L1 -> Disjoint L1 (b :: L2).
proof: Proof. intros a L1 L2 H' H'0; inversion_clear H'. apply DisjointDef; simpl in |- *; auto. intros b H'1; red in |- *; intros H'2; inversion_clear H'2; auto. case H'0; apply InEqComp with (a := b); auto. absurd (InEq b L2); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)