Skip to content

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

Closed
jamesmckinna wants to merge 8 commits into
agda:masterfrom
jamesmckinna:Fin-lower-properties
Closed

[ refactor ] make n≢i : n ≢ toℕ i argument to lower₁ irrelevant#2783
jamesmckinna wants to merge 8 commits into
agda:masterfrom
jamesmckinna:Fin-lower-properties