∀y,x:Top.  (arrow(<x, y>) ~ y)
{ (UnivCD THENA Auto) }
1. y : Top
2. x : Top
⊢ arrow(<x, y>) ~ y