Goal:
    A : Type  R : A → A → bool  R_refl : ∀ x : A, R x x
  ============================
   (is_true (forallb2 R [] []))


DEBUG:Going to execute:
reflexivity
DEBUG LTAC Evaluated term: l