fact: Definition State (S : Set) : S ▷ S := sor {| Operations := λ _, True ; Arities := λ s _, forall s' : S, s = s' ; Sorts := λ s _ _, s |} {| Operations := λ _, S ; Arities := λ _ _, True ; Sorts := λ _ s _, s |}.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple