
Prove lemmas:


needs subsumption strategy

Problem:

 - what is the right formulation of
   the lemma ?

   need universal quantification ?

   {f}{g}{h} ....

 - needs term-depth abstraction
 	otherwise it will loop
