The inductive hypotheses are themselves elim rules: rather specific
ones but, by design, exactly the ones we need to eliminate the
recursive calls. Once we've done that, we get 2x2 cases of failure
or success, propagated by **!^**. We either get compressed versions
of *s* and *t* which we can **^** together, or an
offending position which we can extend with **left** or
**right**.

And that's it.

I wonder how easy it would be to automate this proof. It strikes me
that I should get **checkElim** free of charge, when I decide
to implement the spec by a structural recursion on the tree.
Come to think of it, I should extract the structural recursion from
the structurally monotonic behaviour of **|>** and **put**.
This is what I was aiming at when I was working on a calculus of
`rumours'.

Next: it's a knockout |
Prev: eliminate **thick** |
Up: contents

Conor's Work Page