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


DEBUG:Going to execute:
<coq-core.plugins.ltac::econstructor@0>
Level 1: evaluation returns
inversion_clear H
where
H := H
of type
constr of type tacvalue


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

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

  
  X : Type
  L : list (option X)
  t : list X
  H : None = 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) (None :: L) t)


DEBUG:Going to execute:
inv ltac:(H)
DEBUG LTAC Evaluated term: a
DEBUG LTAC Evaluated term: (map_option_out L)

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

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

  
  X : Type
  L : list (option X)
  t : list X
  H : None = 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) (None :: L) t)


DEBUG:Going to execute:
fun H => inversion_clear H