with-where.agda

Sρ→Tρ : ∀ {Γ Δ}
  → let Γ' = cctx Γ in let Δ' = cctx Δ in
    (∀ {A} → Γ S.∋ A → Δ S.∋ A)
  → T.Renaming Γ' Δ'
Sρ→Tρ {Γ} {Δ} ρ {A'} x with cctx Γ | inspect cctx Γ | cctx Δ | inspect cctx Δ |  ct⁻¹ A' | inspect ct⁻¹ A'
Sρ→Tρ {Γ} {Δ} ρ {A'} x' | Γ' | [ Γ≡Γ' ] | Δ' | [ Δ≡Δ' ] | A | [ A'≡A ] with T∋→S∋ x'
... | x rewrite sym Γ≡Γ' | from∘to Context-iso Γ | xyz = {!S∋→T∋ (ρ x)!}  --  | ct≡ {Conversion.TypeIso.from' A'} | to∘from Type-iso A'
  where
    xyz : ct (Conversion.TypeIso.from' A') ≡ A'
    xyz = to∘from Type-iso A'
    
-- Not in scope:
--   xyz at <...>/Bisimulation.lagda:105,52-55
-- when scope checking xyz