Goal:
    X : Type  t : list X  H : Some [] = Some t
  ============================
   (All2 (λ (x : option X) (y : X), x = Some y) [] t)


DEBUG:Going to execute:
inversion_clear H
DEBUG LTAC Evaluated term: H
DEBUG LTAC Evaluated term: H