Goal:
  
  A : Type
  B : Type
  f : nat → A → B
  f' : nat → A → B
  g : B → bool
  g' : B → bool
  l : list A
  H0 : ∀ (n : nat) (x : A),
         nth_error l n = Some x → g (f (0 + n) x) = g' (f' (0 + n) x)
  ============================
   (forallb g (mapi_rec f l 0) = forallb g' (mapi_rec f' l 0))


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