[ refactor ] make n≢i : n ≢ toℕ i
argument to lower₁
irrelevant
#2783
Loading
n≢i : n ≢ toℕ i
argument to lower₁
irrelevant
#2783