# Pastebin al8q0eud
open import Size
open import Level

data SizedId {ℓ} {A : Size → Set ℓ} (σ : Size) (x : A σ) : A σ → Set (suc ℓ) where
  refl : SizedId σ x x

ssubst : ∀ {ℓ ℓᵇ} {A : Size → Set ℓ} {σ : Size} {x y : A σ} {P : (a : A σ) → Set ℓᵇ} → SizedId {A = A} σ x y → P x → P y
ssubst refl px = px