Is there a lemma that shows `(Σ;;; [] |- t : T) -> (Σ;;; Γ |- t : T)`

(notably, there's no need to subst on closed terms)?

Weakening gives you this, but will have a lift on closed terms

Is there a lemma that lets me get rid of the lift?

(The thing I'm trying to prove right now is

```
forall Γ : context,
wf_local Σ Γ ->
Σ;;; [] |- qP
: tSort
(Universe.lType
{|
t_set :=
{|
LevelExprSet.this := [(Level.level "MetaCoq.Quotation.ToPCUIC.Init.Typing.547", 0)];
LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "MetaCoq.Quotation.ToPCUIC.Init.Typing.547", 0)
|};
t_ne := eq_refl
|}) ->
Σ;;; [] |- qH
: tProd {| binder_name := nAnon; binder_relevance := Relevant |}
(tApp
(tApp
(tApp (tInd {| inductive_mind := (MPfile ["Logic"; "Init"; "Coq"], "eq"); inductive_ind := 0 |} [])
(tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool"); inductive_ind := 0 |} []))
(tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool"); inductive_ind := 0 |} 0 []))
(tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool"); inductive_ind := 0 |} 0 [])) qP ->
Σ;;; Γ
|- tApp qH
(tApp
(tApp (tConstruct {| inductive_mind := (MPfile ["Logic"; "Init"; "Coq"], "eq"); inductive_ind := 0 |} 0 [])
(tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool"); inductive_ind := 0 |} []))
(tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool"); inductive_ind := 0 |} 0 [])) : qP
```

subject to appropriate constraints on `Σ`

. Basically if I have that `qP`

is a type and `qH : true = true -> qP`

, both in the empty context, then I can type `qH (eq_refl true) : qP`

in any context.

Well, lifting a closed term is equivalent to a term, but I guess you don't want that?

`Lemma lift_closed n k t : closedn k t -> lift n k t = t.`

?

Last updated: Jul 23 2024 at 21:01 UTC