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