Enclosed is the file chunnel.pvs. I have been trying to prove the lemma move1_lemma. In so doing I get a subgoal which is now given by the lemma the_subgoal (by inspection it can be seen that this is true). I have already explained the problems with trying to prove this: the commands expand, replace etc don't work. E.g (expand "index") returns 'no change'. Your earlier solution was to use apply-extensionality, however at this stage of the proof this is not sensible, because the resulting extension is over the whole of nat. I have reduced the_subgoal by hand, using the prover to prove the bits and pieces given in lemmas length,index1,index2. The first reduction was to the lemma loopy. However i still have the same problems with trying to prove this. The second reduction,loopy0, allows apply-extensionality to produce an extension over below(2) and the prove is then immediate. Is it a bug? Is there a way out?