Inductive vehicle : Set := bicycle : nat -> vehicle | motorized : nat -> nat -> vehicle. Check vehicle_rec. (* vehicle_rec : forall P : vehicle -> Set, (forall n : nat, P (bicycle n)) -> (forall n n0 : nat, P (motorized n n0)) -> forall v : vehicle, P v *) (* Definition nb_seats (v:vehicle) : nat := does not work *) Definition nb_seats : vehicle -> nat := vehicle_rec (fun v => nat) (fun nseats => nseats) (fun nbseats nwheels => nbseats).