Require Import Facts.

Module Type State.
Parameter state : Type.
Parameter action : Type.
Parameter guard : Type.

Parameter actionE : action → state → state.
Parameter guardE : guard → state → bool.
Coercion actionE : action >-> Funclass.
Coercion guardE : guard >-> Funclass.

Parameter action_eq : action → action → bool.
Parameter guard_eq : guard → guard → bool.
Axiom action_eqP : Equality.axiom action_eq.
Axiom guard_eqP : Equality.axiom guard_eq.
Canonical action_eqMixin := EqMixin action_eqP.
Canonical action_eqType := Eval hnf in EqType action action_eqMixin.
Canonical guard_eqMixin := EqMixin guard_eqP.
Canonical guard_eqType := Eval hnf in EqType guard guard_eqMixin.
End State.

Module Type EqState (Sigma : State).
Import Sigma.

Parameter to_test : state → guard.
Parameter to_testP : Equality.axiom to_test.
Canonical state_eqMixin := EqMixin to_testP.
Canonical state_eqType := Eval hnf in EqType state state_eqMixin.

Lemma to_testT sigma : to_test sigma sigma.
End EqState.