∀g,k,f,T:Top.  (For{T,f,k} x ∈ []. g[x] ~ k)
{ (UnivCD THENA Auto) }
1. g : Top@i
2. k : Top@i
3. f : Top@i
4. T : Top@i
⊢ For{T,f,k} x ∈ []. g[x] ~ k