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.