Library MetaCoq.PCUIC.PCUICAlpha

Section Alpha.
  Context {cf:checker_flags}.

  Lemma build_branches_type_eq_term :
    ∀ p p' ind mdecl idecl pars u brtys,
      eq_term_upto_univ eq eq p p' →
      map_option_out
        (build_branches_type ind mdecl idecl pars u p) =
      Some brtys →
      ∑ brtys',
        map_option_out
          (build_branches_type ind mdecl idecl pars u p') =
        Some brtys' ×
        All2 (on_Trel_eq (eq_term_upto_univ eq eq) snd fst) brtys brtys'.

  Lemma types_of_case_eq_term :
    ∀ ind mdecl idecl npar args u p p' pty indctx pctx ps btys,
      types_of_case ind mdecl idecl (firstn npar args) u p pty =
      Some (indctx, pctx, ps, btys) →
      eq_term_upto_univ eq eq p p' →
      ∑ btys',
        types_of_case ind mdecl idecl (firstn npar args) u p' pty =
        Some (indctx, pctx, ps, btys') ×
        All2 (on_Trel_eq (eq_term_upto_univ eq eq) snd fst) btys btys'.

  Lemma wf_local_nth_error_vass :
    ∀ Σ Γ i na ty,
      wf Σ.1 →
      wf_local Σ Γ →
      nth_error Γ i = Some (vass na ty) →
      lift_typing typing Σ Γ (lift0 (S i) ty) None.

  Lemma fix_context_nth_error :
    ∀ m i d,
      nth_error m i = Some d →
      nth_error (fix_context m) (#|m| - S i) =
      Some (vass (dname d) (lift0 i (dtype d))).

  Lemma nth_error_weak_context :
    ∀ Γ Δ i d,
      nth_error Δ i = Some d →
      nth_error (Γ ,,, Δ) i = Some d.

  Lemma Forall2_eq :
    ∀ A (l l' : list A),
      Forall2 eq l l' →
      l = l'.

  Lemma typing_alpha :
    ∀ Σ Γ u v A,
      wf Σ.1 →
      Σ ;;; Γ |- u : A →
      eq_term_upto_univ eq eq u v →
      Σ ;;; Γ |- v : A.

  Corollary type_nameless :
    ∀ Σ Γ u A,
      wf Σ.1 →
      Σ ;;; Γ |- u : A →
      Σ ;;; Γ |- nl u : A.


  Lemma upto_names_eq_term_upto_univ Re Rle t u
    : eq_term_upto_univ Re Rle t u →
      ∀ t' u', t ≡ t' → u ≡ u' →
               eq_term_upto_univ Re Rle t' u'.

  Lemma upto_names_leq_term φ t u t' u'
    : t ≡ t' → u ≡ u' → leq_term φ t u → leq_term φ t' u'.

  Lemma upto_names_eq_term φ t u t' u'
    : t ≡ t' → u ≡ u' → eq_term φ t u → eq_term φ t' u'.

  Definition upto_names_decl := eq_decl_upto eq.

  Definition upto_names_ctx := eq_context_upto eq.

  Infix "≡Γ" := upto_names_ctx (at level 60).

  Lemma destArity_alpha Γ u v ctx s :
    destArity Γ u = Some (ctx, s) →
    u ≡ v →
    ∑ ctx', destArity Γ v = Some (ctx', s) × ctx ≡Γ ctx'.

  Lemma upto_names_conv_context (Σ : global_env_ext) Γ Δ :
    Γ ≡Γ Δ → conv_context Σ Γ Δ.

  Lemma wf_local_alpha Σ Γ Γ' :
    wf Σ.1 → wf_local Σ Γ → Γ ≡Γ Γ' → wf_local Σ Γ'.

  Lemma isWfArity_alpha Σ Γ u v :
    wf Σ.1 →
    isWfArity typing Σ Γ u →
    u ≡ v →
    isWfArity typing Σ Γ v.

  Lemma upto_names_nl t
    : t ≡ nl t.

  Lemma upto_names_nlctx Γ
    : Γ ≡Γ nlctx Γ.

End Alpha.

Infix "≡Γ" := upto_names_ctx (at level 60).