Applying thickElim rewrites thick w i, instantiating i

Either

• i was w and we got none

  !leaf then propagates the failure; the corresponding goal follows from the failure hypothesis (at position here)

• i was a (thin w j) and we got (some j)

  !leaf then propagates the success; the corresponding goal follows from the success hypothesis (with the compressed witness supplied by thickElim)

But what about the step case? How do we deal with the recursive checks given that checkElim is the theorem we're trying to prove. Well, that's what inductive proof is all about, isn't it?

Next: apply ind hyps | Prev: induction on t | Up: contents