improve strengthening to get cumul info on type

[tabareau]

No description provided.

[MevenBertrand]

We did not use it anywhere, so this is probably nitpicking, but the new phrasing is in some respect weaker than the old one: it does not say anything about terms which have only variable in Δ but a type living in Γ, only about the situation where both the term and the type live in Δ. I'm not sure how to phrase a theorem that would encompass this situation and give you what you want (ie a relation between the old and new type), but maybe:

Theorem typing_renaming_cond_P `{checker_flags} {P f Σ Γ Δ t T} {wfΣ : wf Σ.1} :
  renaming P Σ Γ Δ f ->
  on_ctx_free_vars P Γ ->
  on_free_vars P t ->
  Σ ;;; Γ |- t : T ->
  ∑ T', [× (on_free_vars P T'), (Σ ;;; Γ |- t : T'), (Σ ;;; Γ |- T' <= T) &
  (Σ ;;; Δ |- rename f t : rename f T')].

[tabareau]

@MevenBertrand thx for the comment. Looks good to you now ?

[MevenBertrand]

LGTM! At least, the new version trivially implies the old one. Not entirely happy about having two typing judgements for t and T', one in Γ and one in Δ, but I guess this really is the "strengthening" bit so it is unavoidable.