890   is then recursively called with the simplified derivative, but before

   890   is then recursively called with the simplified derivative, but before

   891   we inject the character @{term c} into value, we need to rectify

   891   we inject the character @{term c} into value, we need to rectify

   892   it (that is construct @{term "f\<^sub>r v"}). We can prove that

   892   it (that is construct @{term "f\<^sub>r v"}). We can prove that

   893 

   893 

   894   \begin{lemma}

   894   \begin{lemma}

   896   \end{lemma}

   896   \end{lemma}

   897 

   897 

   898   \noindent

   898   \noindent

   899   holds but for lack of space refer the reader to our mechanisation for details.

   899   holds but for lack of space refer the reader to our mechanisation for details.

   900 

   900