Neat, thank you!

```
Lemma weakening_typing_from_empty {cf Σ Γ t T}
: @typing cf Σ [] t T -> wf Σ -> wf_local Σ Γ -> @typing cf Σ Γ t T.
Proof.
intros Hty Hwf HΓ.
replace Γ with ([],,, Γ,,, lift_context #|Γ| 0 []);
[ replace t with (lift #|Γ| 0 t) | .. ];
[ replace T with (lift #|Γ| 0 T) | .. ].
{ eapply (@weakening_typing cf Σ Hwf [] [] Γ);
rewrite ?app_context_nil_l; tea. }
all: rewrite ?app_context_nil_l.
all: try now generalize (lift_context_length #|Γ| 0 []); destruct lift_context; cbn; congruence.
all: rewrite lift_closed; try reflexivity.
all: change 0 with #|[]:context|.
all: unshelve ((eapply type_closed + eapply subject_closed); eassumption).
all: assumption.
Qed.
```

Is it worth adding this to `Typing.PCUICClosedTyp`

or `Typing.PCUICWeakeningTyp`

or something?

`weaken_ctx`

with `Γ := []`

?

Ah, yes, thank you!

Jason Gross has marked this topic as resolved.

Last updated: Jul 23 2024 at 21:01 UTC