Hot stripping coqs

Hello proggers.

How do I discharge this goal in Coq?

Inductive type : nat -> Set := ctor : forall n, type n.
Goal forall n, type 0 <> type (S n).

Wizards of the coed halp plox111 How do I make my coq to accept this?

Definition fb (x : bool) : Set := nat.
Definition fn (x : nat) : Set := nat.
Definition depx (b : bool) (x : if b then bool else nat) (y : if b then fb x else fn x) := 0.