proposition: Theorem list_in_cons_app : ∀ A (a : A) x y l, List.In a [x … l ++ [y]] → List.In a [x; y … l].
proof: Proof. intros A a x y l H. simpl in H; simpl. destruct H as [| H]; [ left; assumption | right ]. revert H; clear; intros. induction l as [| x]; intros; [ assumption | simpl ]. simpl in H. destruct H as [H| H]. right; left; assumption. apply IHl in H. destruct H as [H| H]; [ left | right; right ]; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz