Rewrite construct

At the moment, proving theorems is quite cumbersome as soon as we have to rewrite the goal using previously shown equations. This is demonstrated by the below theorem, for example:

define mulOne : forall a, Equality a (mul a (successor Zero)) where
  case mulOne { Zero } => reflexivity
  case mulOne { successor p } =>
    substitute { P = (x => Equality (successor p) x) } Addition.addSuccessor (
      substitute { P = (x => Equality (successor p) (successor x)) } Addition.addZero (          
        congruence successor (mulOne { p })))

The thing is, that the predicate P can be generated by the compiler, as it is the result of the overall goal and the equation (e.g., Addition.addSuccessor) used for the rewrite. Hence, I propose to extend pattern matching similar to Agda as follows:

define mulOne : forall a, Equality a (mul a (successor Zero)) where
  case mulOne { Zero } => reflexivity
  case mulOne { successor p } rewrite Addition.addSuccessor, Addition.addZero =>          
    congruence successor (mulOne { p })

That is, we introduce a sequence of equations at the end of a case, which reflects the sequence of rewrites that should happen before evaluation the body. This is just a shorthand notation for the above, more verbose example.