Library MetaCoq.Erasure.EInduction
Deriving a compact induction principle for terms
Lemma term_forall_list_ind :
∀ P : term → Prop,
(P tBox) →
(∀ n : nat, P (tRel n)) →
(∀ i : ident, P (tVar i)) →
(∀ (n : nat) (l : list term), Forall P l → P (tEvar n l)) →
(∀ (n : name) (t : term), P t → P (tLambda n t)) →
(∀ (n : name) (t : term),
P t → ∀ t0 : term, P t0 → P (tLetIn n t t0)) →
(∀ t u : term, P t → P u → P (tApp t u)) →
(∀ (s : String.string), P (tConst s)) →
(∀ (i : inductive) (n : nat), P (tConstruct i n)) →
(∀ (p : inductive × nat) (t : term),
P t → ∀ l : list (nat × term),
tCaseBrsProp P l → P (tCase p t l)) →
(∀ (s : projection) (t : term), P t → P (tProj s t)) →
(∀ (m : mfixpoint term) (n : nat), Forall (fun x ⇒ P (dbody x)) m → P (tFix m n)) →
(∀ (m : mfixpoint term) (n : nat), Forall (fun x ⇒ P (dbody x)) m → P (tCoFix m n)) →
∀ t : term, P t.
Class Hyp (T : Type) := hyp : T.
Class AHyp (T : Type) := ahyp : T.