prove the following theorem in haskell programming:

THEORY Ex$5$Q$2$

IMPORT$-$THEORY Equality

IMPORT$-$THEORY Boolean

IMPORT$-$THEORY Arithmetic

IMPORT$-$THEORY List

IMPORT$-$HASKELL List

IMPORT$-$HASKELL Ex$5$

THEOREM ex$5$q$2$

frec $18==37$

END ReduceAll

QED ex$5$q$2$

the following is a piece of code given in the main that cannot be edited:

module Ex$5$ where

$--$ no code for Q$1$

$--$ for Q$2$:

frec x $=$ if x $<=8$ then $6$ else x $+$ frec $($x $-5)$

$--$ for Q$3$:

bonus $[]=16$

bonus $($x:xs$)=$ x $+7+$ bonus xs

$--$for Q$4$:

casef x

$|$ x $<9=2*$x

$|$ x $>=9=2*$x$-1$

prove the theorem by editing 'STRATEGY ReduceAll' ONLY