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


DEBUG:Going to execute:
induction L in t, H |- *

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

  
  X : Type
  a : option X
  L : list (option X)
  t : list X
  H : map_option_out (a :: L) = Some t
  IHL : ∀ t : list X,
          map_option_out L = Some t
          → All2 (λ (x : option X) (y : X), x = Some y) L t
  ============================
   (All2 (λ (x : option X) (y : X), x = Some y) (a :: L) t)


DEBUG:Going to execute:
cbn in *
DEBUG LTAC Evaluated term: L