Goal:
  
  A : Type
  P : nat → A → Type
  x : A
  l : list A
  IHl : ∀ k : nat,
          Alli P k l
          → Alli (λ k' : nat, P (Nat.pred #|l| - k' + k)) 0 (List.rev l)
  k : nat
  a : Alli P k l
  b : Alli P (#|l| + k) [x]
  ============================
   (Alli (λ k' : nat, P (Nat.pred #|l ++ [x]| - k' + k)) 0
      (List.rev [x] ++ List.rev l))


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

File "./theories/All_Forall.v", line 1011, characters 33-43:
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/All_Forall.v", line 1011, characters 33-43:
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]