Inductive NativeSize : nat->Prop :=
| n_1 : NativeSize 1
| n_8 : NativeSize 8
| n_16 : NativeSize 16
| n_32 : NativeSize 32
| n_64 : NativeSize 64.

Inductive In : nat -> list nat -> Prop :=
| in_ev : forall x xs, In x (x::xs)
| in_cons : forall x y xs, In x xs -> In x (y::xs).

Fixpoint In (n:nat) (xs:list nat) : Prop :=
match xs with
| nil => False
| x::xs => (x = n) \/ In n xs
end.