∀f,g,s:Top.  (msFor{g} x ∈ 0{s}. f[x] ~ e)
{ (UnivCD THENA Auto) }
1. f : Top
2. g : Top
3. s : Top
⊢ msFor{g} x ∈ 0{s}
    f[x] ~ e