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