∀b,x:Top.  (#(x.b) ~ #(b) + 1)
{ (UnivCD THENA Auto) }
1. b : Top@i
2. x : Top@i
⊢ #(x.b) ~ #(b) + 1