∀[x:Top]. (0 + x ≤ x)
{ xxxSqReasoningxxx }
1. x : Base
2. (0 + x)↓
3. 0 ∈ ℤ
4. x ∈ ℤ
⊢ 0 + x ≤ x