Section experiment.

Inductive state : Type :=

| s1 : state

| s2 : state.

Fixpoint transitions(s:state):state :=

match s with

| s1 => s2

| s2 => s2

end.

Eval compute in (transitions s1).

Example test_transitions:

(transitions (transitions s1)) = s2.

Proof. simpl. reflexivity. Qed.

End experiment.