proposition: Theorem NotInAppendf : forall (L1 L2 : list A) (m : A), ~ InEq m L1 -> ~ InEq m L2 -> ~ InEq m (appendf L1 L2).
proof: Proof. intros L1 L2 m H' H'0; red in |- *; intros H'1. case (appendfInvEq L1 L2 m H'1); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)