Require Import Facts States.
Set Implicit Arguments.

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.
Instance Rename_term : Rename term.
Instance Subst_term : Subst term.
Instance SubstLemmas_term : SubstLemmas term.

End ICSyntax.