Set Implicit Arguments.
Unset Strict Implicit.

Section Ports.

  Variable i o : nat.
  Definition T_Inportno := {x : nat | x < i}.
  Definition T_Outportno := {x : nat | x < o}.

End Ports.