Goal:
    A : Type  P : A → A → Type  r : A  r' : A  X : All2 P [r] ([] ++ [r'])
  ============================
   (All2 P [] [] × P r r')


DEBUG:Going to execute:
inversion X
DEBUG LTAC Evaluated term: l'