Take advantage of eta to clean sigma proofs

Now they use less funext