∀[x,y:ℤ].  uiff(↑x <z y;x < y)
{ Auto }
1. x : ℤ
2. y : ℤ
3. ↑x <z y
⊢ x < y
1. x : ℤ
2. y : ℤ
3. x < y
⊢ ↑x <z y