proposition: Lemma InA_app : forall l1 l2 x, InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
proof: Proof. intros l1; induction l1 as [|a l1 IHl1]; simpl in *; intuition. inv; auto. match goal with H0' : InA _ (l1 ++ _) |- _ => rename H0' into H0 end. elim (IHl1 _ _ H0); auto. Qed.
imports: List Sorted Setoid Basics Morphisms