proposition: Lemma InA_split : forall l x, InA x l -> exists l1 y l2, eqA x y /\ l = l1++y::l2.
proof: Proof. intros l; induction l as [|a l IHl]; intros x H; inv. - exists (@nil A); exists a; exists l; auto. - match goal with H' : InA x l |- _ => rename H' into H0 end. destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))). exists (a::l1); exists y; exists l2; auto. split; simpl; f_equal; auto. Qed.
imports: List Sorted Setoid Basics Morphisms