Goal:
    T : Type  M : Type  R : M -> M -> Prop  m : T -> M
  ============================
   ((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::intro@1> $1