∀x,j,i:Top.  (source(link_x from i to j) ~ i){ (UnivCD THENA Auto) }1. x : Top@i2. j : Top@i3. i : Top@i⊢ source(link_x from i to j) ~ i