Goal:
    A : Type  P : A → Prop  l1 : list A  h1 : Forall P l1
  ============================
   (∀ l2 : list A, Forall P l2 → Forall P (l1 ++ l2))


DEBUG:Going to execute:
induction h1

Goals:
    A : Type  P : A → Prop
  ============================
   (∀ l2 : list A, Forall P l2 → Forall P ([] ++ l2))

  
  A : Type
  P : A → Prop
  x : A
  l : list A
  H : P x
  h1 : Forall P l
  IHh1 : ∀ l2 : list A, Forall P l2 → Forall P (l ++ l2)
  ============================
   (∀ l2 : list A, Forall P l2 → Forall P ((x :: l) ++ l2))


DEBUG:Going to execute:
intros l2 h2
DEBUG LTAC Evaluated term: h1