Library MetaCoq.Erasure.EInversion

Module PA := PCUICAst.
Module P := PCUICWcbvEval.

Lemma type_Case_inv (Σ : global_env_ext) (hΣ : wf Σ.1) Γ ind npar p c brs T :
  Σ;;; Γ |- PCUICAst.tCase (ind, npar) p c brs : T →
  { '(u, args, mdecl, idecl, pty, indctx, pctx, ps, btys) : _ &
         (PCUICTyping.declared_inductive (fst Σ) mdecl ind idecl) ×
         (PCUICAst.ind_npars mdecl = npar) ×
         let pars := firstn npar args in
         (Σ;;; Γ |- p : pty) ×
         (types_of_case ind mdecl idecl pars u p pty = Some (indctx, pctx, ps, btys)) ×
         (check_correct_arity (global_ext_constraints Σ) idecl ind u indctx pars pctx) ×
         (existsb (leb_sort_family (universe_family ps)) (PCUICAst.ind_kelim idecl)) ×
         (Σ;;; Γ |- c : PCUICAst.mkApps (tInd ind u) args) ×
         (All2 (fun x y : nat × PCUICAst.term ⇒ ((fst x = fst y) × (Σ;;; Γ |- snd x : snd y)) × (Σ ;;; Γ |- snd y : tSort ps)) brs btys) ×
         (Σ ;;; Γ |- PCUICAst.mkApps p (skipn npar args ++ [c]) ≤ T)}%type.

Notation type_Construct_inv := PCUICInversion.inversion_Construct.
Notation type_tFix_inv := PCUICInversion.inversion_Fix.

Lemma eval_box_apps:
  ∀ (Σ' : list E.global_decl) (e : E.term) (x x' : list E.term),
    Forall2 (eval Σ') x x' →
    eval Σ' e tBox → eval Σ' (mkApps e x) tBox.