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:
<coq-core.plugins.ltac::cut@0>
DEBUG LTAC Evaluated term: (forall (a : M) (a0 : T),
                            m a0 = a ->
                            Acc
                              ((fun (R : M -> M -> Prop) 
                                  (f : T -> M) (x y : T) => 
                                R (f x) (f y)) R m) a0)
DEBUG LTAC Evaluated term: (forall (a : M) (a0 : T),
                            m a0 = a ->
                            Acc
                              ((fun (R : M -> M -> Prop) 
                                  (f : T -> M) (x y : T) => 
                                R (f x) (f y)) R m) a0)