substituteFilter : { Γ Δ : Ctx b } → TypedFilter ta Γ Δ → Ctx b → Ctx b
  substituteFilter done _ = []
  substituteFilter (yes {ta = h} i) other = h ∷ substituteFilter i other
  substituteFilter (no i)           other = other ++ substituteFilter i other

  substitute :
    { Γ Δ Σ : Ctx b }
    (filter : TypedFilter tb Γ Δ) →
    STLC Γ ta →
    STLC Σ tb →
    STLC (substituteFilter filter Σ) ta
  substitute (no done) var other =  other -- agda's not happy :(