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


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrrewrite@0> $1 $2
Level 1: evaluation returns
<coq-core.plugins.ltac::cut@0>
where
$1 := 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
of type
constr of type tacvalue

DEBUG LTAC Evaluated term: (H (m a))
DEBUG LTAC Evaluated term: (well_founded_ind wf
                              (fun mm : M =>
                               forall a : T, m a = mm -> Acc ?R a))
DEBUG LTAC Evaluated term: Acc_intro

COQC theories/MCList.v
File "./theories/MCList.v", line 19, characters 23-33:
Warning: Notation map_length is deprecated since 8.20.
Use length_map instead.
[deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
File "./theories/MCList.v", line 19, characters 34-44:
Warning: Notation app_length is deprecated since 8.20.
Use length_app instead.
[deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
File "./theories/MCList.v", line 19, characters 45-60:
Warning: Notation rev_length is deprecated since 8.20.
Use length_rev instead.
[deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]