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