Goal:
  
  A : Type
  f : A → bool
  g : nat → A
  n : nat
  fg : ∀ x : nat, x < n → f (g x)
  ============================
   (is_true (forallb f (unfold n g)))


DEBUG:Going to execute:
induction n; simpl
DEBUG LTAC Evaluated term: H