inductive Actus.Closures.Star {α : Type} (r : α → α → Type) : α → α → Type

Star r a b: b is reachable from a in zero or more r-steps.

• refl {α : Type} {r : α → α → Type} {a : α} : Star r a a
• step {α : Type} {r : α → α → Type} {a b c : α} : r a b → Star r b c → Star r a c