proposition: Theorem appendfIncl1 : forall L1 L2 : list A, Disjoint L1 L2 -> incl L1 (appendf L1 L2).
proof: Proof. intros L1 L2 HL1L2. apply appendDisjIncl1 with (L2 := L2); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)