Set Implicit Arguments.

(*Implicit Types s a : Set.*)

Inductive state : Set -> Set -> Type :=
	  mkState (s:Set) (a:Set) (_ : forall foo:s, a*s) : state s a.

Definition runState (s:Set) (a:Set) (st:state s a) : s -> a*s :=
  match st with mkState _ _ f => f end.