Goal:
  
  G : t
  A : Type
  B : Type
  f : A -> B -> A
  g : B -> bool
  a : B
  l : list B
  acc : A
  IHl : forall acc : A,
        fold_left f (filter g l) acc =
        fold_left (fun (acc0 : A) (x : B) => if g x then f acc0 x else acc0)
          l acc
  ============================
   (fold_left f (filter g l) acc =
    fold_left (fun (acc : A) (x : B) => if g x then f acc x else acc) l acc)


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

Goals:

DEBUG:Going to execute:
hnf

Goals:

DEBUG:Going to execute:
intros

Goals:

DEBUG:Going to execute:
solve
[ do
![ solve
 [ trivial | apply : eq_sym ; trivial ]
 | discriminate
 | contradiction
 | Ltac.split ]
| case not_locked_false_eq_true; Ltac.assumption
| match goal with
  | H:~ _ |- _ => solve [ case H; trivial ]
  end ]