Inductive state Type s1 state s2 state Fixpoint transitions state stat

Inductive state : Type :=
  | s1 : state
  | s2 : state.

Fixpoint transitions(s:state):state :=
  match s with
  | s1 => s2
  | s2 => s2
  end.