∀[a,b:Top].  (<a, b> ~ Ax ∈ Type)
{ TACTIC:(UnivCD THENA Auto) }
1. a : Top
2. b : Top
⊢ <a, b> ~ Ax ∈ Type