Lemma term_forall_list_ind :
  ∀ P : term → Prop,
    (∀ n : nat, P (tRel n)) →
    (∀ i : ident, P (tVar i)) →
    (∀ (n : nat) (l : list term), Forall P l → P (tEvar n l)) →
    (∀ s, P (tSort s)) →
    (∀ t : term, P t → ∀ (c : cast_kind) (t0 : term), P t0 → P (tCast t c t0)) →
    (∀ (n : name) (t : term), P t → ∀ t0 : term, P t0 → P (tProd n t t0)) →
    (∀ (n : name) (t : term), P t → ∀ t0 : term, P t0 → P (tLambda n t t0)) →
    (∀ (n : name) (t : term),
        P t → ∀ t0 : term, P t0 → ∀ t1 : term, P t1 → P (tLetIn n t t0 t1)) →
    (∀ t : term, P t → ∀ l : list term, Forall P l → P (tApp t l)) →
    (∀ (s : String.string) (u : list Level.t), P (tConst s u)) →
    (∀ (i : inductive) (u : list Level.t), P (tInd i u)) →
    (∀ (i : inductive) (n : nat) (u : list Level.t), P (tConstruct i n u)) →
    (∀ (p : inductive × nat) (t : term),
        P t → ∀ t0 : term, P t0 → ∀ l : list (nat × term),
            tCaseBrsProp P l → P (tCase p t t0 l)) →
    (∀ (s : projection) (t : term), P t → P (tProj s t)) →
    (∀ (m : mfixpoint term) (n : nat), tFixProp P P m → P (tFix m n)) →
    (∀ (m : mfixpoint term) (n : nat), tFixProp P P m → P (tCoFix m n)) →
    ∀ t : term, P t.

Lemma lift_to_list (P : term → Prop) : (∀ t, wf t → P t) → ∀ l, Forall wf l → Forall P l.

Lemma lift_to_wf_list (P : term → Prop) : ∀ l, Forall (fun t ⇒ wf t → P t) l → Forall wf l → Forall P l.

Lemma term_wf_forall_list_ind :
  ∀ P : term → Prop,
    (∀ n : nat, P (tRel n)) →
    (∀ i : ident, P (tVar i)) →
    (∀ (n : nat) (l : list term), Forall P l → P (tEvar n l)) →
    (∀ s, P (tSort s)) →
    (∀ t : term, P t → ∀ (c : cast_kind) (t0 : term), P t0 → P (tCast t c t0)) →
    (∀ (n : name) (t : term), P t → ∀ t0 : term, P t0 → P (tProd n t t0)) →
    (∀ (n : name) (t : term), P t → ∀ t0 : term, P t0 → P (tLambda n t t0)) →
    (∀ (n : name) (t : term),
        P t → ∀ t0 : term, P t0 → ∀ t1 : term, P t1 → P (tLetIn n t t0 t1)) →
    (∀ t : term, isApp t = false → wf t → P t →
                      ∀ l : list term, l ≠ nil → Forall wf l → Forall P l → P (tApp t l)) →
    (∀ (s : String.string) (u : list Level.t), P (tConst s u)) →
    (∀ (i : inductive) (u : list Level.t), P (tInd i u)) →
    (∀ (i : inductive) (n : nat) (u : list Level.t), P (tConstruct i n u)) →
    (∀ (p : inductive × nat) (t : term),
        P t → ∀ t0 : term, P t0 → ∀ l : list (nat × term),
            tCaseBrsProp P l → P (tCase p t t0 l)) →
    (∀ (s : projection) (t : term), P t → P (tProj s t)) →
    (∀ (m : mfixpoint term) (n : nat), tFixProp P P m → Forall (fun def ⇒ isLambda (dbody def) = true) m → P (tFix m n)) →
    (∀ (m : mfixpoint term) (n : nat), tFixProp P P m → P (tCoFix m n)) →
    ∀ t : term, wf t → P t.