proposition: Theorem fappendfInvEq : forall (L1 L2 : list A) (m : A), InEq m (fappendf L1 L2) -> InEq m L1 \/ InEq m (map f L2).
proof: Proof. intros L1 L2 m H'. apply appendEqInv with (L3 := fappendf L1 L2); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)