Library MetaCoq.Erasure.EArities

Lemma isErasable_Proof Σ Γ t :
  Is_proof Σ Γ t → isErasable Σ Γ t.

Lemma it_mkProd_isArity:
  ∀ (l : list context_decl) A,
    isArity A →
    isArity (it_mkProd_or_LetIn l A).

Lemma isArity_ind_type (Σ : global_env_ext) mind ind idecl :
  wf Σ →
  declared_inductive (fst Σ) mind ind idecl →
  isArity (ind_type idecl).

Lemma isWfArity_prod_inv:
  ∀ (Σ : global_env_ext) (Γ : context) (x : name) (x0 x1 : term),
    isWfArity typing Σ Γ (tProd x x0 x1) → (∑ s : universe, Σ;;; Γ |- x0 : tSort s) × isWfArity typing Σ (Γ,, vass x x0) x1
.

Lemma isArity_subst:
  ∀ x2 : term, ∀ s n, isArity x2 → isArity (subst s n x2).

Lemma isArity_typing_spine:
  ∀ (Σ : global_env_ext) (Γ : context) (L : list term) (T x4 : term),
    wf Σ → wf_local Σ Γ →
    Is_conv_to_Arity Σ Γ x4 → typing_spine Σ Γ x4 L T → Is_conv_to_Arity Σ Γ T.

Lemma inds_nth_error ind u l n t :
  nth_error (inds ind u l) n = Some t → ∃ n, t = tInd {| inductive_mind := ind ; inductive_ind := n |} u.

Lemma it_mkProd_arity :
  ∀ (l : list context_decl) (A : term), isArity (it_mkProd_or_LetIn l A) → isArity A.

Lemma isArity_mkApps t L : isArity (mkApps t L) → isArity t ∧ L = [].

Lemma typing_spine_red :
  ∀ (Σ : PCUICAst.global_env_ext) Γ (args args' : list PCUICAst.term) (X : All2 (red Σ Γ) args args') (bla : wf Σ)
    (T x x0 : PCUICAst.term) (t0 : typing_spine Σ Γ x args x0) (c : Σ;;; Γ |- x0 ≤ T) (x1 : PCUICAst.term)
    (c0 : Σ;;; Γ |- x1 ≤ x), isWfArity_or_Type Σ Γ T → typing_spine Σ Γ x1 args' T.

Lemma invert_it_Ind_red1 Σ L i u l t Γ : wf Σ →
  red1 Σ Γ (it_mkProd_or_LetIn L (mkApps (tInd i u) l)) t → ∃ L' l', t = it_mkProd_or_LetIn L' (mkApps (tInd i u) l').

Lemma invert_it_Ind_red Σ L i u l t Γ : wf Σ →
  red Σ Γ (it_mkProd_or_LetIn L (mkApps (tInd i u) l)) t → ∃ L' l', t = it_mkProd_or_LetIn L' (mkApps (tInd i u) l').

Lemma it_mkProd_red_Arity Σ c0 i u l : wf Σ →
  ¬ Is_conv_to_Arity Σ [] (it_mkProd_or_LetIn c0 (mkApps (tInd i u) l)).

Lemma invert_it_Ind_eq_prod:
  ∀ (u : universe_instance) (i : inductive) (x : name) (x0 x1 : term) (x2 : context) (x3 : list term),
    tProd x x0 x1 = it_mkProd_or_LetIn x2 (mkApps (tInd i u) x3) → ∃ (L' : context) (l' : list term), x1 = it_mkProd_or_LetIn L' (mkApps (tInd i u) l').

Lemma tConstruct_no_Type (Σ : global_env_ext) ind c u x1 : wf Σ →
  isErasable Σ [] (mkApps (tConstruct ind c u) x1) →
  Is_proof Σ [] (mkApps (tConstruct ind c u) x1).

Inductive conv_decls (Σ : global_env_ext) Γ (Γ' : context) : ∀ (x y : context_decl), Type :=
| conv_vass : ∀ (na na' : name) (T T' : term),
                
                Σ;;; Γ |- T = T' → conv_decls Σ Γ Γ' (vass na T) (vass na' T')
| conv_vdef_type : ∀ (na : name) (b T : term),
    
    conv_decls Σ Γ Γ' (vdef na b T) (vdef na b T).

Lemma conv_context_refl (Σ : global_env_ext) Γ :
  wf Σ → wf_local Σ Γ →
  context_relation (@conv_decls Σ) Γ Γ.

Lemma context_conversion_red1 (Σ : global_env_ext) Γ Γ' s t : wf Σ →
   context_relation (@conv_decls Σ) Γ Γ' → red1 Σ Γ s t → red Σ Γ' s t.

Lemma context_conversion_red (Σ : global_env_ext) Γ Γ' s t : wf Σ →
  context_relation (@conv_decls Σ) Γ Γ' → red Σ Γ s t → red Σ Γ' s t.

Lemma isWfArity_or_Type_red:
  ∀ (Σ : global_env_ext) (Γ : context) (T : term), wf Σ → wf_local Σ Γ →
    isWfArity_or_Type Σ Γ T → ∀ x5 : term, red Σ Γ T x5 → isWfArity_or_Type Σ Γ x5.

Lemma is_prop_sort_sup:
  ∀ x1 x2 : universe, is_prop_sort (Universe.sup x1 x2) → is_prop_sort x2.

Lemma is_prop_sort_prod x2 x3 :
  is_prop_sort (Universe.sort_of_product x2 x3) → is_prop_sort x3.

Lemma sort_typing_spine:
  ∀ (Σ : global_env_ext) (Γ : context) (L : list term) (u : universe) (x x0 : term),
    wf Σ →
    is_prop_sort u →
    typing_spine Σ Γ x L x0 → Σ;;; Γ |- x : tSort u → ∑ u', Σ;;; Γ |- x0 : tSort u' × is_prop_sort u'.

Lemma arity_type_inv (Σ : global_env_ext) Γ t T1 T2 : wf Σ → wf_local Σ Γ →
  Σ ;;; Γ |- t : T1 → isArity T1 → Σ ;;; Γ |- t : T2 → Is_conv_to_Arity Σ Γ T2.

Lemma Is_type_app (Σ : global_env_ext) Γ t L T :
  wf Σ →
  wf_local Σ Γ →
  Σ ;;; Γ |- mkApps t L : T →
  isErasable Σ Γ t →
  ∥isErasable Σ Γ (mkApps t L)∥.

Lemma Is_type_lambda (Σ : global_env_ext) Γ na T1 t :
  wf Σ →
  wf_local Σ Γ →
  isErasable Σ Γ (tLambda na T1 t) →
  ∥isErasable Σ (vass na T1 :: Γ) t∥.

Lemma Is_type_red (Σ : global_env_ext) Γ t v:
  wf Σ →
  red Σ Γ t v →
  isErasable Σ Γ t →
  isErasable Σ Γ v.

Lemma Is_type_eval (Σ : global_env_ext) Γ t v:
  wf Σ →
  eval Σ Γ t v →
  isErasable Σ Γ t →
  isErasable Σ Γ v.