Goal:
  
  T : Type
  M : Type
  R : M -> M -> Prop
  m : T -> M
  wf : forall a : M, Acc R a
  ============================
   (forall a : T, Acc (fun x y : T => R (m x) (m y)) a)


DEBUG:Going to execute:
cut
            (forall (a : M) (a0 : T),
             m a0 = a -> Acc ((fun R f x y => R (f x) (f y)) R m) a0)