proposition: Theorem appendDisjIncl1 : forall L1 L2 L3 : list A, append L1 L2 L3 -> Disjoint L1 L2 -> incl L1 L3.
proof: Proof. intros L1 L2 L3 H'; elim H'; auto with datatypes core. intros L4 H'0; red in |- *; intros a H'1; inversion H'1. intros a b L4 L5 L6 H'0 H'1 H'2 H'3; inversion_clear H'3. lapply (H a); [ intros H'4; case H'4 | idtac ]; auto. intros a b L4 L5 L6 H'0 H'1 H'2 H'3; apply incl_cons with (A := A); auto with datatypes core; apply incl_tran with (m := L6); auto with datatypes core. apply H'2; apply DisjointInv2 with (a := a); auto. intros a b L4 L5 L6 H'0 H'1 H'2 H'3; apply incl_tran with (m := L6); simpl in |- *; auto with datatypes core. apply H'2; apply DisjointInv1 with (a := b); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)