Require Export Arith.
Require Export ZArith.
Require Export List.
Require Export Peano_dec.
Require Export PAutoMod.

Parameter Sig : Time.
Parameter Lambda : Time.
Parameter n : nat.

Inductive VarName : Set :=
  | Sender_x : VarName
  | Bus_y : VarName.

Definition TypeVarName (n : VarName) :=
  match n return Set with
  | Sender_x ⇒ Time
  | Bus_y ⇒ Time
  end.

Module Globals.
Definition V := VarName.
Definition TV := TypeVarName.
End Globals.

Module AutoLGen := AutoL_general Globals.