proposition: Theorem appendfInv : forall (L1 L2 : list A) (m : A), In m (appendf L1 L2) -> In m L1 \/ In m L2.
proof: Proof. intros L1 L2 m H'. apply appendInv with (L3 := appendf L1 L2); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)