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:
fun $1 => <coq-core.plugins.ltac::cut@0>