Require Import Facts States.
Set Implicit Arguments.
Unset Strict Implicit.

Module ICSyntax (Sigma : State).
Export Sigma.

Inductive term :=
| Act (a : action) (s : term)
| If (b : guard) (s t : term)
| Def (s t : {bind term})
| Jump (f : var).

Instance Ids_term : Ids term. derive. Defined.
Instance Rename_term : Rename term. derive. Defined.
Instance Subst_term : Subst term. derive. Defined.
Instance SubstLemmas_term : SubstLemmas term. derive. Qed.

End ICSyntax.