Goal:
    A : Type  l : list A  i : nat  Hi : i < #|l|
  ============================
   (nth_error (List.rev l) i = nth_error l (#|l| - S i))


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrrewrite@0> $1 $2

File "./theories/MCList.v", line 874, characters 25-40:
Warning: Notation List.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]
File "./theories/MCList.v", line 874, characters 25-40:
Warning: Notation List.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]
File "./theories/MCList.v", line 874, characters 25-40:
Warning: Notation List.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]
File "./theories/MCList.v", line 874, characters 25-40:
Warning: Notation List.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]
File "./theories/MCList.v", line 874, characters 25-40:
Warning: Notation List.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]
File "./theories/MCList.v", line 874, characters 25-40:
Warning: Notation List.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]
Goals:
    A : Type  l : list A  i : nat  Hi : i < #|l|
  ============================
   (i < #|l|)

    A : Type  l : list A  i : nat  Hi : i < #|l|
  ============================
   (nth_error (List.rev (List.rev l)) (#|l| - S i) = nth_error l (#|l| - S i))


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: nth_error_rev
DEBUG LTAC Evaluated term: nth_error_rev
DEBUG LTAC Evaluated term: length_rev
DEBUG LTAC Evaluated term: length_rev
DEBUG LTAC Evaluated term: length_rev
DEBUG LTAC Evaluated term: length_rev
DEBUG LTAC Evaluated term: length_rev
DEBUG LTAC Evaluated term: length_rev

Goals:
    A : Type  l : list A  i : nat  Hi : i < #|l|
  ============================
   (i < #|l|)

    A : Type  l : list A  i : nat  Hi : i < #|l|
  ============================
   (nth_error (List.rev (List.rev l)) (#|l| - S i) = nth_error l (#|l| - S i))


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3