Hi, I am now struggling with structural induction, this cannot be proved so I needed to prove with stronger property but I am stuck... please help with proving..

so, this is based on Haskell property (tree structure)

so 'Haskell' definition of binary tree is

data Tree a = Nul

| Node a (Tree a) (Tree a)

so basically, if the tree has no node then it is Nul or otherwise tree a has node a and left to it another tree that has less number than a and another tree on the right with the number greater than Node a.

so the problem has this property.

mult Nul = 1 ------ (M1)

mult (Node a t1 t2) = a * mult t1 * mult t2 ------ (M2)

multa t = multb t 1 ------ (MA)

multb Nul acc = acc --------- (MB1)

multb (Node a t1 t2) acc = multb t1 (a * (multb t2 acc)) ---- (MB2)

and I need to prove

mult t = multa t

certain two cannot be equal hence must prove with stronger property...

it seems that multb is acc times multiplication all nodes but I don't know how to prove from this point..

help me thank you very much for your support always..