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


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>