1 2 3 4 5 6 7 8 9
Inductive state : Type := | s1 : state | s2 : state. Fixpoint transitions(s:state):state := match s with | s1 => s2 | s2 => s2 end.