Goal:
  
  A : Type
  P : list A → list A → A → A → Type
  X : ∀ (n : nat) (x1 x2 : A),
        n < 0
        → nth_error [] n = Some x1
          → nth_error [] n = Some x2 → P [] (skipn (S n) []) x1 x2
  ============================
   (All2_fold P [] [])


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