Goal:
    A : Type  P : A → A → Type  hp : CRelationClasses.Reflexive P  x : list A
  ============================
   (∀ x : A, P x x)


DEBUG:Going to execute:
intros
DEBUG LTAC Evaluated term: All2_refl