Simple question COQ

I'm a beginner in the coq proof assistant, so sorry if my question is silly. I would like to prove properties of a mathematical object. For clarity I will describe an over-simplified version of my object. Intuitively, the object has
three sets A, B, C. The list A is of the form
$$A= \{(0,x_1) (0,x_2), ... ,(0,x_n)\}$$ i.e, all pairs consist of the number zero and an arbitrary number. Analogously, the set B is of the form
$$B = \{(1,y_1)(1,y_2)...(1,y_m)\}$$. And the set $C$ is such that C = A U B.
For concreteness the sets $A,B,C$ can be defined as lists, if for some reason it is not inconvenient in Coq

So the simplified object would be of the following form:

Object

A : Set of elements of the form (0,x) where x is some number

B : Set of elements of the form (1,y) where x is some number

C : Set such that C = A U B

The Condition that the structure must satisfy is:

If (0,a) belongs to A then (1,a) belongs to B.

Questions:

1) How do I define a type consisting of pairs in which the
first element is 0 and the second an arbitrary natural number?
(Obs: This was answered by @KonstantinWeitz but his answer received
a minus. Why wouldn't Konstantin's answer be satisfactory in Coq?)

2)How do I define the object above in coq? I tried to do it with records.
But the problem is that I have no idea of how to define a type of question 1.

3) How to I impose the condition that this object is valid only if for
each (0,x_n) in A there is a (1,y_n) in B with y_n=x_n? And the condition
that $C = A \cup B$?

Set-theoretic thinking is creating trouble, as you are trying
to do things in non-Coq ways. Let me show you a solution which
works better, and then you can explain what your actual non-simplified
problem is -- we can probably optimize that one to.

If we have two lists A and B then we do not have to tag the elements
of the first list with 0 and the second one with 1. That is, rather
than having


A = [(0,x_1), ..., (n,x_n)] and B = [(1,y_1), ..., (m, y_m)]

we can equivalently have just


A = [x_1, ..., x_n] and B = [y_1, ..., y_m].

So, we are really trying to define:


A pair of lists such that the elements of the first one are contained in the second one.

We are going to use the standard library for lists (by the way
if you are simulating sets by using lists, you shouldn't).

Require Import List.

(* We define what it means for the elements of list X to be
   contained in list Y. *)
Definition contained_in {T} (X : list T) (Y : list T) :=
   forall x, In x X -> In x Y.

(* Now we define our data structure. It is a Record with three fields. *)
Record MyLists := {
  A : list nat;
  B : list nat;
  valid : contained_in A B
}.

(** For example, suppose we want to construct A = [1,2,3] and B = [2,3,3,1,5]. *)
Definition example : MyLists.
Proof.
  (* We give Coq the fields we know about. *)
  refine {| A := 1::2::3::nil ; B := 2::3::3::1::5::nil |}.
  (* Coq tells us we also have to provide the 'valid' field. *)
  (* We tell Coq to do it itself. *)
  firstorder.
Defined.

StackExchange Computer Science Q#32707, answer score: 2