∀vars,R,K:Top.  (K-forces(K;R(vars)) ~ λi,a. i,a |= R(vars)){ (UnivCD THENA Auto) }1. vars : Top2. R : Top3. K : Top⊢ K-forces(K;R(vars)) ~ λi,a. i,a |= R(vars)