∀b,a:Top.  (zip([a / b];[]) ~ [])
{ (UnivCD THENA Auto) }
1. b : Top@i
2. a : Top@i
⊢ zip([a / b];[]) ~ []