improve commute-subst-rename

[damhiya]

The commute-subst-rename lemma in the Substitution chapter quantifies over polymorphic renaming ρ : ∀{Γᵨ} → Rename Γᵨ (Γᵨ , ★) (i.e. the ρ itself quantifies over the context Γᵨ), but the parameter Γᵨ is only instantiated with Γᵨ = Γ and Γᵨ = Δ. Thus we can replace this with just two renamings ρ₁ : Rename Γ (Γ , ★) and ρ₂ : Rename Δ (Δ , ★). By this way, we can also avoid defining some what awkward ρ′. I think the resulting proof is more clean.

I also fixed the corresponding prose below the agda code. It seems that the equational reasoning part was just broken, for example in this line:

          ≡ rename S_ (exts σ (ρ y))
          ≡ rename S_ (rename S_ (σ (ρ y)      (by the premise)

which should be

          ≡ rename S_ (exts σ (ρ y))
          ≡ rename S_ (rename ρ (σ y))         (by the premise)

even if we keep using polymorphic renaming.

[wadler]

Thank you, SoonWon. I'm not sure how to judge the difference between the two proofs. Yours is more general, which is a plus, but the single polymorphic rename may be closer to how one should think of the situation. Since @jsiek wrote this chapter, he should decide. (And an extra thanks for correcting the prose, which is important in any case.)

[jsiek]

Thanks, these changes look good to me!