Proof Compression

[marcusrossel]

mkCongrOf can support multiple cHoles at once, so when we have multiple subsequent rewrites which do not overlap (that is, the subexpression position of one is not a prefix of the other), perform both steps at once. I'm not sure how this jibes with tracing as that relies on single steps. But perhaps tracing can force proof reconstruction back into using single steps.