Goal:
    A : Type  P : A → A → Type  l : list A  HP : ∀ x : A, P x x
  ============================
   (All2 P l l)


DEBUG:Going to execute:
induction l; constructor
DEBUG LTAC Evaluated term: andb_and
DEBUG LTAC Evaluated term: andb_and
DEBUG LTAC Evaluated term: equiv_reflectT
DEBUG LTAC Evaluated term: All3_forallb3
DEBUG LTAC Evaluated term: forallb3_All3