proposition: Lemma InA_app_iff : forall l1 l2 x, InA x (l1 ++ l2) <-> InA x l1 \/ InA x l2.
proof: Proof. split. - apply InA_app. - destruct 1 as [H|H]; generalize H; do 2 rewrite InA_alt. + destruct 1 as (y,(H1,H2)); exists y; split; auto. apply in_or_app; auto. + destruct 1 as (y,(H1,H2)); exists y; split; auto. apply in_or_app; auto. Qed.
imports: List Sorted Setoid Basics Morphisms