Library lts

Section LTS.
Variable Event: Type.

Record LTS: Type := mkLTS {
        State: Type;
        LEvent: Type;
        Init: State → Prop;
        Next: State → (Event + LEvent) → State → Prop
}.

End LTS.