proposition: Theorem appendDisjoint : forall L1 L2 L3 : list A, append L1 L2 L3 -> forall L4 : list A, Disjoint L1 L4 -> Disjoint L2 L4 -> Disjoint L3 L4.
proof: Proof. intros L1 L2 L3 H'; elim H'; auto. intros a b L4 L5 L6 H'0 H'1 H'2 L7 H'3 H'4. apply DisjointCons2; auto. apply H'2; auto. apply DisjointInv2 with (a := a); auto. apply DisjointInv2 with (a := b); auto. inversion_clear H'3; auto. intros a b L4 L5 L6 H'0 H'1 H'2 L7 H'3 H'4; apply DisjointCons2; auto. apply H'2; auto. apply DisjointInv2 with (a := a); auto. inversion_clear H'3; auto. intros a b L4 L5 L6 H'0 H'1 H'2 L7 H'3 H'4; apply DisjointCons2; auto. apply H'2; auto. apply DisjointInv2 with (a := b); auto. inversion_clear H'4; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)