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.

Fixpoint ntrans (n:nat) (s:state) :=

match n with

| 0 => s

| S n' => ntrans n' (transitions s)

end.

Lemma ntrans_const: forall n s, n>0 -> ntrans n s = s2.

Proof.

intuition.

Qed.

End experiment.