Add fold operator to STS

[javierdiaz72]

This PR adds a fold operator to STS.

[WhatisRT]

I think a comment would be nice here. From what I can tell, if you have a relation that relates some states given some inputs, you can show that it if it holds for the states of a single step and with no step, then it also holds for arbitrarily many steps with the closure relation. It took me a few minutes to figure this out, so it'd be nice if the next person didn't have to.

[WhatisRT]

Suggested change

	(∀ {i is} → Trans (_⊢_—[ i ]→_ γ) (P is) (P (i ∷ is))) →
	(∀ {i is} → Trans (γ ⊢_—[ i ]→_) (P is) (P (i ∷ is))) →

I think this is more readable. You can do the same thing 2 lines below.

[javierdiaz72]

That's exactly what I wanted to do but an error about ambiguous parsing showed up, although that happened in another context in which I first developed the function. So, I've just fixed it in 0760676.

[javierdiaz72]

I think a comment would be nice here. From what I can tell, if you have a relation that relates some states given some inputs, you can show that it if it holds for the states of a single step and with no step, then it also holds for arbitrarily many steps with the closure relation. It took me a few minutes to figure this out, so it'd be nice if the next person didn't have to.

Fixed in 20ec33c.